Metamath Proof Explorer

Theorem peano5nni

Description: Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of Apostol p. 34. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion peano5nni ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ℕ ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 df-nn ⊢ ℕ = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) “ ω )
2 df-ima ⊢ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) “ ω ) = ran ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
3 1 2 eqtri ⊢ ℕ = ran ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
4 frfnom ⊢ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) Fn ω
5 4 a1i ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) Fn ω )
6 fveq2 ⊢ ( 𝑦 = ∅ → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) )
7 6 eleq1d ⊢ ( 𝑦 = ∅ → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ↔ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ 𝐴 ) )
8 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) )
9 8 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ↔ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 ) )
10 fveq2 ⊢ ( 𝑦 = suc 𝑧 → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) )
11 10 eleq1d ⊢ ( 𝑦 = suc 𝑧 → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ↔ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) ∈ 𝐴 ) )
12 ax-1cn ⊢ 1 ∈ ℂ
13 fr0g ⊢ ( 1 ∈ ℂ → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1 )
14 12 13 ax-mp ⊢ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) = 1
15 simpl ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → 1 ∈ 𝐴 )
16 14 15 eqeltrid ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ ∅ ) ∈ 𝐴 )
17 oveq1 ⊢ ( 𝑥 = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) → ( 𝑥 + 1 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) )
18 17 eleq1d ⊢ ( 𝑥 = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) → ( ( 𝑥 + 1 ) ∈ 𝐴 ↔ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ 𝐴 ) )
19 18 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ 𝐴 ) )
20 19 ad2antlr ⊢ ( ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ 𝐴 ) )
21 ovex ⊢ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ V
22 eqid ⊢ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
23 oveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 + 1 ) = ( 𝑛 + 1 ) )
24 oveq1 ⊢ ( 𝑦 = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) → ( 𝑦 + 1 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) )
25 22 23 24 frsucmpt2 ⊢ ( ( 𝑧 ∈ ω ∧ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ V ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) )
26 21 25 mpan2 ⊢ ( 𝑧 ∈ ω → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) )
27 26 eleq1d ⊢ ( 𝑧 ∈ ω → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) ∈ 𝐴 ↔ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ 𝐴 ) )
28 27 adantl ⊢ ( ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) ∈ 𝐴 ↔ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) + 1 ) ∈ 𝐴 ) )
29 20 28 sylibrd ⊢ ( ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) ∈ 𝐴 ) )
30 29 expcom ⊢ ( 𝑧 ∈ ω → ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ suc 𝑧 ) ∈ 𝐴 ) ) )
31 7 9 11 16 30 finds2 ⊢ ( 𝑦 ∈ ω → ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ) )
32 31 com12 ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( 𝑦 ∈ ω → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ) )
33 32 ralrimiv ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ∀ 𝑦 ∈ ω ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 )
34 ffnfv ⊢ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) : ω ⟶ 𝐴 ↔ ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) Fn ω ∧ ∀ 𝑦 ∈ ω ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ‘ 𝑦 ) ∈ 𝐴 ) )
35 5 33 34 sylanbrc ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) : ω ⟶ 𝐴 )
36 35 frnd ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ran ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω ) ⊆ 𝐴 )
37 3 36 eqsstrid ⊢ ( ( 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 + 1 ) ∈ 𝐴 ) → ℕ ⊆ 𝐴 )