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	⊢ ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 )
Assertion	find	⊢ 𝐴 = ω

Proof

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