Theorem finxp3o

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

	Ref	Expression
Assertion	finxp3o	⊢ ( 𝑈 ↑↑ 3o ) = ( ( 𝑈 × 𝑈 ) × 𝑈 )

Proof

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