Theorem finxp2o

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

	Ref	Expression
Assertion	finxp2o	$$⊢U\uparrow \uparrow 2_{𝑜}=U\times U$$

Proof

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