Theorem find 4111

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. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)

Hypothesis

Ref	Expression
find.1	|- (A C_ om /\ (/) e. A /\ A.x e. A suc x e. A)

Assertion

Ref	Expression
find	|- A = om

Distinct variable group:   x,A

Proof of Theorem find

Step	Hyp	Ref	Expression
1		find.1	. . 3 |- (A C_ om /\ (/) e. A /\ A.x e. A suc x e. A)
2	1	simp1i 1129	. 2 |- A C_ om
3		3simpc 1119	. . . . 5 |- ((A C_ om /\ (/) e. A /\ A.x e. A suc x e. A) -> ((/) e. A /\ A.x e. A suc x e. A))
4	1, 3	ax-mp 7	. . . 4 |- ((/) e. A /\ A.x e. A suc x e. A)
5		df-ral 2359	. . . . . 6 |- (A.x e. A suc x e. A <-> A.x(x e. A -> suc x e. A))
6		alral 2404	. . . . . 6 |- (A.x(x e. A -> suc x e. A) -> A.x e. om (x e. A -> suc x e. A))
7	5, 6	sylbi 225	. . . . 5 |- (A.x e. A suc x e. A -> A.x e. om (x e. A -> suc x e. A))
8	7	anim2i 539	. . . 4 |- (((/) e. A /\ A.x e. A suc x e. A) -> ((/) e. A /\ A.x e. om (x e. A -> suc x e. A)))
9	4, 8	ax-mp 7	. . 3 |- ((/) e. A /\ A.x e. om (x e. A -> suc x e. A))
10		peano5 4109	. . 3 |- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om C_ A)
11	9, 10	ax-mp 7	. 2 |- om C_ A
12	2, 11	eqssi 2861	1 |- A = om

Syntax hints:   -> wi 3   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  A.wral 2355   C_ wss 2827  (/)c0 3082  suc csuc 3813  omcom 4085

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086

Copyright terms: Public domain