Theorem finxp2o

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

	Ref	Expression
Assertion	finxp2o	⊢ ( 𝑈 ↑↑ 2o ) = ( 𝑈 × 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2		finxpeq2	⊢ ( 2o = suc 1o → ( 𝑈 ↑↑ 2o ) = ( 𝑈 ↑↑ suc 1o ) )
3	1 2	ax-mp	⊢ ( 𝑈 ↑↑ 2o ) = ( 𝑈 ↑↑ suc 1o )
4		1onn	⊢ 1o ∈ ω
5		1n0	⊢ 1o ≠ ∅
6		finxpsuc	⊢ ( ( 1o ∈ ω ∧ 1o ≠ ∅ ) → ( 𝑈 ↑↑ suc 1o ) = ( ( 𝑈 ↑↑ 1o ) × 𝑈 ) )
7	4 5 6	mp2an	⊢ ( 𝑈 ↑↑ suc 1o ) = ( ( 𝑈 ↑↑ 1o ) × 𝑈 )
8		finxp1o	⊢ ( 𝑈 ↑↑ 1o ) = 𝑈
9	8	xpeq1i	⊢ ( ( 𝑈 ↑↑ 1o ) × 𝑈 ) = ( 𝑈 × 𝑈 )
10	3 7 9	3eqtri	⊢ ( 𝑈 ↑↑ 2o ) = ( 𝑈 × 𝑈 )