Theorem om2

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

	Ref	Expression
Assertion	om2	|- ( 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		omsuc	|- ( ( 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		om1	|- ( 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 ) )