# 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)

Ref Expression
Hypothesis find.1 ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 )
Assertion find 𝐴 = ω

### Proof

Step Hyp Ref Expression
1 find.1 ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 )
2 1 simp1i 𝐴 ⊆ ω
3 3simpc ( ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 ) )
4 1 3 ax-mp ( ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 )
5 df-ral ( ∀ 𝑥𝐴 suc 𝑥𝐴 ↔ ∀ 𝑥 ( 𝑥𝐴 → suc 𝑥𝐴 ) )
6 alral ( ∀ 𝑥 ( 𝑥𝐴 → suc 𝑥𝐴 ) → ∀ 𝑥 ∈ ω ( 𝑥𝐴 → suc 𝑥𝐴 ) )
7 5 6 sylbi ( ∀ 𝑥𝐴 suc 𝑥𝐴 → ∀ 𝑥 ∈ ω ( 𝑥𝐴 → suc 𝑥𝐴 ) )
8 7 anim2i ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥𝐴 suc 𝑥𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥𝐴 → suc 𝑥𝐴 ) ) )
9 4 8 ax-mp ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥𝐴 → suc 𝑥𝐴 ) )
10 peano5 ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥𝐴 → suc 𝑥𝐴 ) ) → ω ⊆ 𝐴 )
11 9 10 ax-mp ω ⊆ 𝐴
12 2 11 eqssi 𝐴 = ω