Metamath Proof Explorer

Theorem peano2nn

Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano2nn ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω
2 fvelrnb ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω → ( 𝐴 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 ) )
3 1 2 ax-mp ⊢ ( 𝐴 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ↔ ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 )
4 ovex ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) ∈ V
5 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
6 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 + 1 ) = ( 𝑥 + 1 ) )
7 oveq1 ⊢ ( 𝑧 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) → ( 𝑧 + 1 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) )
8 5 6 7 frsucmpt2 ⊢ ( ( 𝑦 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) )
9 4 8 mpan2 ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑦 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) )
10 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
11 fnfvelrn ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) Fn ω ∧ suc 𝑦 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) )
12 1 10 11 sylancr ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) )
13 df-nn ⊢ ℕ = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω )
14 df-ima ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
15 13 14 eqtri ⊢ ℕ = ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
16 12 15 eleqtrrdi ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑦 ) ∈ ℕ )
17 9 16 eqeltrrd ⊢ ( 𝑦 ∈ ω → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) ∈ ℕ )
18 oveq1 ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) = ( 𝐴 + 1 ) )
19 18 eleq1d ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 → ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) + 1 ) ∈ ℕ ↔ ( 𝐴 + 1 ) ∈ ℕ ) )
20 17 19 syl5ibcom ⊢ ( 𝑦 ∈ ω → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 → ( 𝐴 + 1 ) ∈ ℕ ) )
21 20 rexlimiv ⊢ ( ∃ 𝑦 ∈ ω ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = 𝐴 → ( 𝐴 + 1 ) ∈ ℕ )
22 3 21 sylbi ⊢ ( 𝐴 ∈ ran ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) → ( 𝐴 + 1 ) ∈ ℕ )
23 22 15 eleq2s ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )