Theorem oe2

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

	Ref	Expression
Assertion	oe2	|- ( A e. On -> ( A .o A ) = ( A ^o 2o ) )

Proof

Step	Hyp	Ref	Expression
1		df-2o	|- 2o = suc 1o
2	1	oveq2i	|- ( A ^o 2o ) = ( A ^o suc 1o )
3		1on	|- 1o e. On
4		oesuc	|- ( ( A e. On /\ 1o e. On ) -> ( A ^o suc 1o ) = ( ( A ^o 1o ) .o A ) )
5	3 4	mpan2	|- ( A e. On -> ( A ^o suc 1o ) = ( ( A ^o 1o ) .o A ) )
6		oe1	|- ( A e. On -> ( A ^o 1o ) = A )
7	6	oveq1d	|- ( A e. On -> ( ( A ^o 1o ) .o A ) = ( A .o A ) )
8	5 7	eqtrd	|- ( A e. On -> ( A ^o suc 1o ) = ( A .o A ) )
9	2 8	eqtr2id	|- ( A e. On -> ( A .o A ) = ( A ^o 2o ) )