Theorem om2

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

	Ref	Expression
Assertion	om2	⊢ ( 𝐴 ∈ 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		omsuc	⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 ·o suc 1o ) = ( ( 𝐴 ·o 1o ) +o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o suc 1o ) = ( ( 𝐴 ·o 1o ) +o 𝐴 ) )
6		om1	⊢ ( 𝐴 ∈ 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 ) )