Theorem finxp3o

Description: The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020)

	Ref	Expression
Assertion	finxp3o	$$⊢U\uparrow \uparrow 3_{𝑜}=\left(U\times U\right)\times U$$

Proof

Step	Hyp	Ref	Expression
1		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
2		finxpeq2	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}\to U\uparrow \uparrow 3_{𝑜}=U\uparrow \uparrow \mathrm{suc}{2}_{𝑜}$$
3	1 2	ax-mp	$$⊢U\uparrow \uparrow 3_{𝑜}=U\uparrow \uparrow \mathrm{suc}{2}_{𝑜}$$
4		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
5		2on0	$$⊢2_{𝑜}\ne \varnothing$$
6		finxpsuc	$$⊢\left(2_{𝑜}\in \mathrm{\omega }\wedge 2_{𝑜}\ne \varnothing \right)\to U\uparrow \uparrow \mathrm{suc}{2}_{𝑜}=U\uparrow \uparrow 2_{𝑜}\times U$$
7	4 5 6	mp2an	$$⊢U\uparrow \uparrow \mathrm{suc}{2}_{𝑜}=U\uparrow \uparrow 2_{𝑜}\times U$$
8		finxp2o	$$⊢U\uparrow \uparrow 2_{𝑜}=U\times U$$
9	8	xpeq1i	$$⊢U\uparrow \uparrow 2_{𝑜}\times U=\left(U\times U\right)\times U$$
10	3 7 9	3eqtri	$$⊢U\uparrow \uparrow 3_{𝑜}=\left(U\times U\right)\times U$$