There are less than \( \# \mu \) atom conditions as \( \# \kappa {\lt} \# \mu \) and \( \# \mu \) is a strong limit. There are less than \( \# \mu \) inflexible \( \beta \)-paths, as each is determined by three type indices less than \( \beta \) and a path with maximum less than \( \beta \), of which there are \( \# \mu \)-many. There are less than \( \# \mu \)-many coding functions of any type \( \delta {\lt} \beta \), because König’s theorem gives

where the last equality follows from the facts that \( \# \{ \delta {\lt} \beta \} \) has cardinality less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \) and that \( \# \mu \) is a strong limit. There are less than \( \# \mu \) \( \delta \)-trees of relations on \( \kappa \) for each \( \delta \leq \alpha \), because there are less than \( \# \mu \)-many relations on \( \kappa \) as \( \# \mu \) is a strong limit, allowing us to conclude by one of the remarks in definition 2.11. Hence there are less than \( \# \mu \) \( \beta \)-near-litter conditions. We can again apply the result about cardinalities of types of trees to deduce that there are less than \( \# \mu \) \( \beta \)-trees of enumerations of atom conditions and of \( \beta \)-near-litter conditions, as required.

Let \( S \) be a support, and let \( T \) be a strong support such that \( S \preceq T \), which exists by proposition 5.4. Then simply define \( R^{\mathcal A}\) and \( R^{\mathcal N}\) to be the required relations.

Let \( W = (R^{\mathcal A}, R^{\mathcal N}, \sigma ) \), and let \( U, V \) be strong supports such that \( \operatorname {\mathsf{spec}}(U) = \sigma = \operatorname {\mathsf{spec}}(V) \), \( S \preceq U, T \preceq V \), and

By proposition 5.21, there is an allowable permutation \( \rho \) such that \( \rho (U) = V \). We claim that \( \rho (S) = T \). Suppose \( (i, a) \in S_A^{\mathcal A}\). Then as \( S \preceq U \), there is \( j \) such that \( (j, a) \in U_A^{\mathcal A}\). So there is \( a' \) such that \( (i, a') \in T_A^{\mathcal A}\) and \( (j, a') \in V_A^{\mathcal A}\). Then \( a' = \rho _A(a) \) as \( \rho (U) = V \), as required. The same simple calculation gives the required result for near-litters.

Follows directly from proposition 5.33 and the remark that there are less than \( \# \mu \) \( \beta \)-trees of relations on \( \kappa \).

Define a function from the type of \( \beta \)-support orbits into the type of weak \( \beta \)-specifications by mapping a representative to a weak specification that specifies it; one will always exist by proposition 5.35. This is an injection: if \( o_1, o_2 \) are orbits with representatives \( S_1, S_2 \) and \( S_1, S_2 \) have the same assigned weak specification, then by proposition 5.36 there is an allowable permutation \( \rho \) such that \( \rho (S_1) = S_2 \), and so \( o_1 = o_2 \). So we are done as there are less than \( \# \mu \) weak \( \beta \)-specifications by proposition 5.37.

Every \( \beta \)-coding function is of the form \( \chi _{(x, S)} \) where \( S \) is a representative chosen in advance for a support orbit, and \( x \) is an object that \( S \) supports under the action of \( \beta \)-allowable permutations. So there are at most

coding functions, which is less than \( \# \mu \).

By proposition 5.39, it suffices to show that there are less than \( \# \mu \) \( \bot \)-support orbits and that there is a bound less than \( \# \mu \) on the amount of objects that a given \( \bot \)-support supports. The first result follows from proposition 5.38, which has vacuous assumptions in this case. The second result follows from applying proposition 5.32 to singletons of atoms, after applying the bijections between \( \bot \)-supports and base supports, and between \( \bot \)-allowable permutations and base permutations.

Again, we apply proposition 5.39. The first claim follows from proposition 5.38, where this time we use the fact that there are less than \( \# \mu \) \( \bot \)-coding functions (proposition 5.40). The second claim follows from proposition 5.32 to \( \bot \)-extensions of type \( \beta \) objects, noting that \( \beta \)-supports correspond to base supports and that \( \beta \)-allowable permutations correspond to base permutations. ¹ The fact that \( \beta \)-allowable permutations correspond to base permutations relies on the fact that we can construct a \( \beta \)-permutation from a base permutation using coherent data (definition 2.25).

A \( (\gamma ,\beta ) \)-raised singleton \( \operatorname {\mathsf{raise}}(S,u) = \chi _{(\operatorname {\mathsf{singleton}}_\beta (u), S + \operatorname {\mathsf{dsupp}}(u)^\beta )} \) is determined by a triple \( (R, o, \chi ) \) where

• \( R \) is the \( \beta \)-tree given by \( R_A = i \) when \( S_A = (i, f) \);

• \( o \) is the support orbit of \( S + \operatorname {\mathsf{dsupp}}(u)^\beta \); and

• \( \chi \) is the coding function \( \chi _{(u, \operatorname {\mathsf{dsupp}}(u))} \).

Indeed, suppose \( \operatorname {\mathsf{raise}}(S, u) \) and \( \operatorname {\mathsf{raise}}(T, v) \) have the same triple \( (R, o, \chi ) \). We must show that

Then there is a \( \beta \)-allowable \( \rho \) such that \( \rho (S + \operatorname {\mathsf{dsupp}}(u)^\beta ) = T + \operatorname {\mathsf{dsupp}}(v)^\beta \), and as they have the same tree \( R \), we can decompose this into \( \rho (S) = T \) and \( \rho (\operatorname {\mathsf{dsupp}}(u)^\beta ) = \operatorname {\mathsf{dsupp}}(v)^\beta \). In particular, \( \rho _\beta (\operatorname {\mathsf{dsupp}}(u)) = \operatorname {\mathsf{dsupp}}(v) \). As \( \chi _{(u, \operatorname {\mathsf{dsupp}}(u))} = \chi _{(v, \operatorname {\mathsf{dsupp}}(v))} \), there is a \( \gamma \)-allowable permutation \( \rho ' \) such that \( \rho '(u) = v \) and \( \rho '(\operatorname {\mathsf{dsupp}}(u)) = \operatorname {\mathsf{dsupp}}(v) \). Hence \( \rho _\beta (u) = v \). This gives

as required.

Now, it remains to show that there are less than \( \# \mu \) such triples \( (R, o, \chi ) \). But this follows directly from proposition 5.38 and the assumption on the cardinalities of the types of coding functions.

By induction we may assume that for all type indices \( \delta {\lt} \beta \), there are strictly less than \( \# \mu \)-many \( \delta \)-coding functions. By ??, we may assume that \( \beta \) is a proper type index, and that it is not minimal in \( \lambda \), so there is some proper type index \( \gamma {\lt} \beta \). By proposition 5.29, every \( \beta \)-coding function is determined by a set of \( (\gamma ,\beta ) \)-raised singletons \( s \) and support orbit \( o \). The conclusion then follows from ?? and the fact that \( \# \mu \) is a strong limit.

If \( \beta \) is \( \bot \), we already know \( \# \mathsf{TSet}_\bot = \# {\mathcal A}= \# \mu \), so suppose \( \# \beta \) is a proper type index. Each object \( x : \mathsf{TSet}_\beta \) is determined by a \( \beta \)-coding function and a \( \beta \)-support. Since there are less than \( \# \mu \)-many \( \beta \)-coding functions (proposition 5.43) and there are exactly \( \# \mu \) \( \beta \)-supports, we obtain \( \# \mathsf{TSet}_\beta \leq \# \mu \). Since the typed near-litter map \( {\mathcal N}\to \mathsf{TSet}_\beta \) is injective, there are at least \( \# {\mathcal N}= \# \mu \) inhabitants of \( \mathsf{TSet}_\beta \), giving the result by antisymmetry.

Use proposition 5.44 and the fact that there are precisely \( \# \mu \)-many \( \beta \)-supports.