Theorem oa0

Description: Addition with zero. Proposition 8.3 of TakeutiZaring p. 57. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	oa0	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		oav	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 +o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ ∅ ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ ∅ ) )
4		rdg0g	⊢ ( 𝐴 ∈ On → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ ∅ ) = 𝐴 )
5	3 4	eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )