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 C_ _om /\ (/) e. A /\ A. x e. A suc x e. A )
Assertion	find	|- A = _om

Proof

Step	Hyp	Ref	Expression
1		find.1	|- ( A C_ _om /\ (/) e. A /\ A. x e. A suc x e. A )
2	1	simp1i	|- A C_ _om
3		3simpc	|- ( ( A C_ _om /\ (/) e. A /\ A. x e. A suc x e. A ) -> ( (/) e. A /\ A. x e. A suc x e. A ) )
4		df-ral	|- ( A. x e. A suc x e. A <-> A. x ( x e. A -> suc x e. A ) )
5		alral	|- ( A. x ( x e. A -> suc x e. A ) -> A. x e. _om ( x e. A -> suc x e. A ) )
6	4 5	sylbi	|- ( A. x e. A suc x e. A -> A. x e. _om ( x e. A -> suc x e. A ) )
7	6	anim2i	|- ( ( (/) e. A /\ A. x e. A suc x e. A ) -> ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) )
8	1 3 7	mp2b	|- ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) )
9		peano5	|- ( ( (/) e. A /\ A. x e. _om ( x e. A -> suc x e. A ) ) -> _om C_ A )
10	8 9	ax-mp	|- _om C_ A
11	2 10	eqssi	|- A = _om