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 ⊢ A ∈ ω → ∅ + 𝑜 A = A

Proof

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