Commutativity, associativity, distributivity and monotonicity of $\oplus$ and $\otimes$, the unit laws, the two exponent laws, and $\kappa \le \lambda$ if and only if $\kappa$ injects into $\lambda$

First half of (a): if $\kappa \le \lambda$ then $\kappa \subseteq \lambda$ by [L5] and the inclusion is an injection, so $\kappa ⪯\lambda$; conversely, if $\kappa ⪯\lambda$ and $\lambda \in \kappa$ then $\lambda \subseteq \kappa$ gives $\lambda ⪯\kappa$, so $\kappa \approx \lambda$ by [L4], contradicting [L7] since $\lambda \in \kappa$; trichotomy then leaves $\kappa \le \lambda$.

The maps $(0,\xi )\mapsto (1,\xi )$, $(1,\eta )\mapsto (0,\eta )$ and $(\xi ,\eta )\mapsto (\eta ,\xi )$ are their own inverses up to relabelling, hence bijections $\kappa \bigsqcup \lambda \to \lambda \bigsqcup \kappa$ and $\kappa \times \lambda \to \lambda \times \kappa$.

The maps $(0,(0,\xi ))\mapsto (0,\xi )$, $(0,(1,\eta ))\mapsto (1,(0,\eta ))$, $(1,\zeta )\mapsto (1,(1,\zeta ))$ and $((\xi ,\eta ),\zeta )\mapsto (\xi ,(\eta ,\zeta ))$ have evident two-sided inverses, hence are bijections $(\kappa \bigsqcup \lambda )\bigsqcup \mu \to \kappa \bigsqcup (\lambda \bigsqcup \mu )$ and $(\kappa \times \lambda )\times \mu \to \kappa \times (\lambda \times \mu )$.

The map $(\xi ,(0,\eta ))\mapsto (0,(\xi ,\eta ))$, $(\xi ,(1,\zeta ))\mapsto (1,(\xi ,\zeta ))$ is a bijection $\kappa \times (\lambda \bigsqcup \mu )\to (\kappa \times \lambda )\bigsqcup (\kappa \times \mu )$.

Unit computations: $\kappa \bigsqcup 0=\{0\}\times \kappa \approx \kappa$; $\kappa \times 0=\mathrm{\varnothing }=0$; $\kappa \times 1=\kappa \times \{0\}\approx \kappa$; ${}^0\kappa =\{\mathrm{\varnothing }\}$ has the empty function as its only element, so ${}^0\kappa \approx 1$; ${}^1\kappa \approx \kappa$ by $h\mapsto h(0)$; ${}^{\kappa }1$ has the constant function $0$ as its only element, so ${}^{\kappa }1\approx 1$; and for $\kappa \mathrm{\ne }0$ there is no function $\kappa \to \mathrm{\varnothing }$, so ${}^{\kappa }0=\mathrm{\varnothing }=0$.

Two bijections of function spaces: $h\mapsto (\xi \mapsto h(0,\xi ),\eta \mapsto h(1,\eta ))$ is a bijection ${}^{\lambda \bigsqcup \mu }\kappa \to ({}^{\lambda }\kappa )\times ({}^{\mu }\kappa )$, with inverse gluing a pair back into one function; and $F\mapsto ((\xi ,\eta )\mapsto F(\eta )(\xi ))$ is a bijection ${}^{\mu }({}^{\lambda }\kappa )\to {}^{\lambda \times \mu }\kappa$, with inverse $f\mapsto (\eta \mapsto (\xi \mapsto f(\xi ,\eta )))$.

Monotonicity injections, for $\kappa \subseteq \lambda$: $\kappa \bigsqcup \mu \subseteq \lambda \bigsqcup \mu$ and $\kappa \times \mu \subseteq \lambda \times \mu$ and ${}^{\mu }\kappa \subseteq {}^{\mu }\lambda$ are inclusions; and for $\mu \mathrm{\ne }0$, extending a function by the constant value $0\in \mu$ on $\lambda \setminus \kappa$ is an injection ${}^{\kappa }\mu \to {}^{\lambda }\mu$, injective because restricting back to $\kappa$ recovers the original function.

Second half of (a): if $A⪯B$ with both well-orderable then $\mid A\mid \approx A⪯B\approx \mid B\mid$ by [L1], so $\mid A\mid ⪯\mid B\mid$ by [L6], and step 1.1 applied to these two cardinals gives $\mid A\mid \le \mid B\mid$.

Claims (b) and (c): by [L1] the sets $\kappa \oplus \lambda$ and $\kappa \bigsqcup \lambda$ are equinumerous, and likewise for $\otimes$, so [L2] lets every outer operation be computed on the untagged representatives; steps 1.2, 1.3 and 1.4 then equate the two underlying sets up to $\approx$, and [L1] gives the same least ordinal on both sides.

Claim (d) is step 1.5 read through [L3] and [L1]: each computed set is equinumerous with $\kappa$, with $1$, or with $0$, and its cardinality is the corresponding cardinal by [L1].

Claim (f): $\lambda \oplus \mu \approx \lambda \bigsqcup \mu$ and ${\kappa }^{\lambda }\approx {}^{\lambda }\kappa$ by [L1], so [L2] and step 1.6 give ${}^{\lambda \oplus \mu }\kappa \approx ({}^{\lambda }\kappa )\times ({}^{\mu }\kappa )$ and ${}^{\mu }({\kappa }^{\lambda })\approx {}^{\lambda \times \mu }\kappa$; taking cardinalities through [L1] and [L3] yields ${\kappa }^{\lambda \oplus \mu }={\kappa }^{\lambda }\otimes {\kappa }^{\mu }$ and $({\kappa }^{\lambda }{)}^{\mu }={\kappa }^{\lambda \otimes \mu }$.

Claim (e): each map of step 1.7 is an injection between the underlying sets, so step 2.1 applied to it gives the corresponding inequality of cardinalities, which by [L3] is the stated inequality of cardinals.

All six claims are established, in ZF except for the exponentials of clauses (e) and (f), which are read under the Axiom of Choice by [L8].