Metamath Proof Explorer


Theorem finxp2o

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

Ref Expression
Assertion finxp2o U ↑↑ 2 𝑜 = U × U

Proof

Step Hyp Ref Expression
1 df-2o 2 𝑜 = suc 1 𝑜
2 finxpeq2 2 𝑜 = suc 1 𝑜 U ↑↑ 2 𝑜 = U ↑↑ suc 1 𝑜
3 1 2 ax-mp U ↑↑ 2 𝑜 = U ↑↑ suc 1 𝑜
4 1onn 1 𝑜 ω
5 1n0 1 𝑜
6 finxpsuc 1 𝑜 ω 1 𝑜 U ↑↑ suc 1 𝑜 = U ↑↑ 1 𝑜 × U
7 4 5 6 mp2an U ↑↑ suc 1 𝑜 = U ↑↑ 1 𝑜 × U
8 finxp1o U ↑↑ 1 𝑜 = U
9 8 xpeq1i U ↑↑ 1 𝑜 × U = U × U
10 3 7 9 3eqtri U ↑↑ 2 𝑜 = U × U