This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) = 𝐴 )