Theorem om1

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. (Contributed by NM, 29-Oct-1995)

	Ref	Expression
Assertion	om1	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 1o ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	oveq2i	⊢ ( 𝐴 ·o 1o ) = ( 𝐴 ·o suc ∅ )
3		peano1	⊢ ∅ ∈ ω
4		onmsuc	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ω ) → ( 𝐴 ·o suc ∅ ) = ( ( 𝐴 ·o ∅ ) +o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o suc ∅ ) = ( ( 𝐴 ·o ∅ ) +o 𝐴 ) )
6	2 5	syl5eq	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 1o ) = ( ( 𝐴 ·o ∅ ) +o 𝐴 ) )
7		om0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
8	7	oveq1d	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ·o ∅ ) +o 𝐴 ) = ( ∅ +o 𝐴 ) )
9		oa0r	⊢ ( 𝐴 ∈ On → ( ∅ +o 𝐴 ) = 𝐴 )
10	6 8 9	3eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 1o ) = 𝐴 )