Theorem oe2

Description: Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025)

	Ref	Expression
Assertion	oe2	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 𝐴 ) = ( 𝐴 ↑o 2o ) )

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2	1	oveq2i	⊢ ( 𝐴 ↑o 2o ) = ( 𝐴 ↑o suc 1o )
3		1on	⊢ 1o ∈ On
4		oesuc	⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 ↑o suc 1o ) = ( ( 𝐴 ↑o 1o ) ·o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o suc 1o ) = ( ( 𝐴 ↑o 1o ) ·o 𝐴 ) )
6		oe1	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o 1o ) = 𝐴 )
7	6	oveq1d	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ↑o 1o ) ·o 𝐴 ) = ( 𝐴 ·o 𝐴 ) )
8	5 7	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o suc 1o ) = ( 𝐴 ·o 𝐴 ) )
9	2 8	eqtr2id	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 𝐴 ) = ( 𝐴 ↑o 2o ) )