Theorem nna0r

Description: Addition to zero. Remark in proof of Theorem 4K(2) of Enderton p. 81. Note: In this and later theorems, we deliberately avoid the more general ordinal versions of these theorems (in this case oa0r ) so that we can avoid ax-rep , which is not needed for finite recursive definitions. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Assertion	nna0r	⊢ ( 𝐴 ∈ ω → ( ∅ +o 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = ∅ → ( ∅ +o 𝑥 ) = ( ∅ +o ∅ ) )
2		id	⊢ ( 𝑥 = ∅ → 𝑥 = ∅ )
3	1 2	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o ∅ ) = ∅ ) )
4		oveq2	⊢ ( 𝑥 = 𝑦 → ( ∅ +o 𝑥 ) = ( ∅ +o 𝑦 ) )
5		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
6	4 5	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o 𝑦 ) = 𝑦 ) )
7		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( ∅ +o 𝑥 ) = ( ∅ +o suc 𝑦 ) )
8		id	⊢ ( 𝑥 = suc 𝑦 → 𝑥 = suc 𝑦 )
9	7 8	eqeq12d	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o suc 𝑦 ) = suc 𝑦 ) )
10		oveq2	⊢ ( 𝑥 = 𝐴 → ( ∅ +o 𝑥 ) = ( ∅ +o 𝐴 ) )
11		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
12	10 11	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( ∅ +o 𝑥 ) = 𝑥 ↔ ( ∅ +o 𝐴 ) = 𝐴 ) )
13		0elon	⊢ ∅ ∈ On
14		oa0	⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
15	13 14	ax-mp	⊢ ( ∅ +o ∅ ) = ∅
16		peano1	⊢ ∅ ∈ ω
17		nnasuc	⊢ ( ( ∅ ∈ ω ∧ 𝑦 ∈ ω ) → ( ∅ +o suc 𝑦 ) = suc ( ∅ +o 𝑦 ) )
18	16 17	mpan	⊢ ( 𝑦 ∈ ω → ( ∅ +o suc 𝑦 ) = suc ( ∅ +o 𝑦 ) )
19		suceq	⊢ ( ( ∅ +o 𝑦 ) = 𝑦 → suc ( ∅ +o 𝑦 ) = suc 𝑦 )
20	19	eqeq2d	⊢ ( ( ∅ +o 𝑦 ) = 𝑦 → ( ( ∅ +o suc 𝑦 ) = suc ( ∅ +o 𝑦 ) ↔ ( ∅ +o suc 𝑦 ) = suc 𝑦 ) )
21	18 20	syl5ibcom	⊢ ( 𝑦 ∈ ω → ( ( ∅ +o 𝑦 ) = 𝑦 → ( ∅ +o suc 𝑦 ) = suc 𝑦 ) )
22	3 6 9 12 15 21	finds	⊢ ( 𝐴 ∈ ω → ( ∅ +o 𝐴 ) = 𝐴 )