HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 find.1 . . 3 |- (A C_ om /\ (/) e. A /\ A.x e. A suc x e. A)
21simp1i 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))
41, 3ax-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))
75, 6sylbi 225 . . . . 5 |- (A.x e. A suc x e. A -> A.x e. om (x e. A -> suc x e. A))
87anim2i 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)))
94, 8ax-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)
119, 10ax-mp 7 . 2 |- om C_ A
122, 11eqssi 2861 1 |- A = om
Colors of variables: wff set class
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