MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  finds Structured version   Visualization version   GIF version

Theorem finds 7598
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.)
Hypotheses
Ref Expression
finds.1 (𝑥 = ∅ → (𝜑𝜓))
finds.2 (𝑥 = 𝑦 → (𝜑𝜒))
finds.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
finds.4 (𝑥 = 𝐴 → (𝜑𝜏))
finds.5 𝜓
finds.6 (𝑦 ∈ ω → (𝜒𝜃))
Assertion
Ref Expression
finds (𝐴 ∈ ω → 𝜏)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem finds
StepHypRef Expression
1 finds.5 . . . . 5 𝜓
2 0ex 5197 . . . . . 6 ∅ ∈ V
3 finds.1 . . . . . 6 (𝑥 = ∅ → (𝜑𝜓))
42, 3elab 3653 . . . . 5 (∅ ∈ {𝑥𝜑} ↔ 𝜓)
51, 4mpbir 234 . . . 4 ∅ ∈ {𝑥𝜑}
6 finds.6 . . . . . 6 (𝑦 ∈ ω → (𝜒𝜃))
7 vex 3483 . . . . . . 7 𝑦 ∈ V
8 finds.2 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜒))
97, 8elab 3653 . . . . . 6 (𝑦 ∈ {𝑥𝜑} ↔ 𝜒)
107sucex 7516 . . . . . . 7 suc 𝑦 ∈ V
11 finds.3 . . . . . . 7 (𝑥 = suc 𝑦 → (𝜑𝜃))
1210, 11elab 3653 . . . . . 6 (suc 𝑦 ∈ {𝑥𝜑} ↔ 𝜃)
136, 9, 123imtr4g 299 . . . . 5 (𝑦 ∈ ω → (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑}))
1413rgen 3143 . . . 4 𝑦 ∈ ω (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑})
15 peano5 7595 . . . 4 ((∅ ∈ {𝑥𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑})) → ω ⊆ {𝑥𝜑})
165, 14, 15mp2an 691 . . 3 ω ⊆ {𝑥𝜑}
1716sseli 3948 . 2 (𝐴 ∈ ω → 𝐴 ∈ {𝑥𝜑})
18 finds.4 . . 3 (𝑥 = 𝐴 → (𝜑𝜏))
1918elabg 3652 . 2 (𝐴 ∈ ω → (𝐴 ∈ {𝑥𝜑} ↔ 𝜏))
2017, 19mpbid 235 1 (𝐴 ∈ ω → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  {cab 2802  wral 3133  wss 3919  c0 4275  suc csuc 6180  ωcom 7570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317  ax-un 7451
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-br 5053  df-opab 5115  df-tr 5159  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-om 7571
This theorem is referenced by:  findsg  7599  findes  7602  seqomlem1  8076  nna0r  8225  nnm0r  8226  nnawordi  8237  nneob  8269  nneneq  8691  pssnn  8727  inf3lem1  9082  inf3lem2  9083  cantnfval2  9123  cantnfp1lem3  9134  r1fin  9193  ackbij1lem14  9647  ackbij1lem16  9649  ackbij1  9652  ackbij2lem2  9654  ackbij2lem3  9655  infpssrlem4  9720  fin23lem14  9747  fin23lem34  9760  itunitc1  9834  ituniiun  9836  om2uzuzi  13317  om2uzlti  13318  om2uzrdg  13324  uzrdgxfr  13335  hashgadd  13739  mreexexd  16915  satfrel  32639  satfdm  32641  satfrnmapom  32642  satf0op  32649  satf0n0  32650  sat1el2xp  32651  fmlafvel  32657  fmlaomn0  32662  gonar  32667  goalr  32669  satffun  32681  trpredmintr  33095  findfvcl  33825  finxp00  34731
  Copyright terms: Public domain W3C validator