Metamath Proof Explorer

Theorem find

Description: The Principle of Finite Induction (mathematical induction). Corollary 7.31 of TakeutiZaring p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that A is a set of natural numbers, zero belongs to A , and given any member of A the member's successor also belongs to A . The conclusion is that every natural number is in A . (Contributed by NM, 22-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Wolf Lammen, 28-May-2024)

Ref Expression
Hypothesis find.1 ⊢ A ⊆ ω ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
Assertion find ⊢ A = ω

Proof

Step Hyp Ref Expression
1 find.1 ⊢ A ⊆ ω ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
2 1 simp1i ⊢ A ⊆ ω
3 3simpc ⊢ A ⊆ ω ∧ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A → ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A
4 df-ral ⊢ ∀ x ∈ A suc ⁡ x ∈ A ↔ ∀ x x ∈ A → suc ⁡ x ∈ A
5 alral ⊢ ∀ x x ∈ A → suc ⁡ x ∈ A → ∀ x ∈ ω x ∈ A → suc ⁡ x ∈ A
6 4 5 sylbi ⊢ ∀ x ∈ A suc ⁡ x ∈ A → ∀ x ∈ ω x ∈ A → suc ⁡ x ∈ A
7 6 anim2i ⊢ ∅ ∈ A ∧ ∀ x ∈ A suc ⁡ x ∈ A → ∅ ∈ A ∧ ∀ x ∈ ω x ∈ A → suc ⁡ x ∈ A
8 1 3 7 mp2b ⊢ ∅ ∈ A ∧ ∀ x ∈ ω x ∈ A → suc ⁡ x ∈ A
9 peano5 ⊢ ∅ ∈ A ∧ ∀ x ∈ ω x ∈ A → suc ⁡ x ∈ A → ω ⊆ A
10 8 9 ax-mp ⊢ ω ⊆ A
11 2 10 eqssi ⊢ A = ω