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	⊢ 𝐴 = ω