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

Theorem finds2 7893
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.)
Hypotheses
Ref Expression
finds2.1 (𝑥 = ∅ → (𝜑𝜓))
finds2.2 (𝑥 = 𝑦 → (𝜑𝜒))
finds2.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
finds2.4 (𝜏𝜓)
finds2.5 (𝑦 ∈ ω → (𝜏 → (𝜒𝜃)))
Assertion
Ref Expression
finds2 (𝑥 ∈ ω → (𝜏𝜑))
Distinct variable groups:   𝑥,𝑦,𝜏   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)

Proof of Theorem finds2
StepHypRef Expression
1 finds2.4 . . . . 5 (𝜏𝜓)
2 0ex 5307 . . . . . 6 ∅ ∈ V
3 finds2.1 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜓))
43imbi2d 340 . . . . . 6 (𝑥 = ∅ → ((𝜏𝜑) ↔ (𝜏𝜓)))
52, 4elab 3668 . . . . 5 (∅ ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜓))
61, 5mpbir 230 . . . 4 ∅ ∈ {𝑥 ∣ (𝜏𝜑)}
7 finds2.5 . . . . . . 7 (𝑦 ∈ ω → (𝜏 → (𝜒𝜃)))
87a2d 29 . . . . . 6 (𝑦 ∈ ω → ((𝜏𝜒) → (𝜏𝜃)))
9 vex 3478 . . . . . . 7 𝑦 ∈ V
10 finds2.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
1110imbi2d 340 . . . . . . 7 (𝑥 = 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜒)))
129, 11elab 3668 . . . . . 6 (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜒))
139sucex 7796 . . . . . . 7 suc 𝑦 ∈ V
14 finds2.3 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝜑𝜃))
1514imbi2d 340 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜃)))
1613, 15elab 3668 . . . . . 6 (suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜃))
178, 12, 163imtr4g 295 . . . . 5 (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)}))
1817rgen 3063 . . . 4 𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})
19 peano5 7886 . . . 4 ((∅ ∈ {𝑥 ∣ (𝜏𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏𝜑)})
206, 18, 19mp2an 690 . . 3 ω ⊆ {𝑥 ∣ (𝜏𝜑)}
2120sseli 3978 . 2 (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏𝜑)})
22 abid 2713 . 2 (𝑥 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜑))
2321, 22sylib 217 1 (𝑥 ∈ ω → (𝜏𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  {cab 2709  wral 3061  wss 3948  c0 4322  suc csuc 6366  ωcom 7857
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7858
This theorem is referenced by:  finds1  7894  onnseq  8346  nnacl  8613  nnmcl  8614  nnecl  8615  nnacom  8619  nnaass  8624  nndi  8625  nnmass  8626  nnmsucr  8627  nnmcom  8628  nnmordi  8633  omsmolem  8658  isinf  9262  isinfOLD  9263  unblem2  9298  fiint  9326  dffi3  9428  card2inf  9552  cantnfle  9668  cantnflt  9669  cantnflem1  9686  cnfcom  9697  trcl  9725  fseqenlem1  10021  nnadju  10194  infpssrlem3  10302  fin23lem26  10322  axdc3lem2  10448  axdc4lem  10452  axdclem2  10517  wunr1om  10716  wuncval2  10744  tskr1om  10764  grothomex  10826  peano5nni  12219  precsexlem6  27885  precsexlem7  27886  peano5n0s  27923  neibastop2lem  35548  finxpreclem6  36580  domalom  36588  oaabsb  42346
  Copyright terms: Public domain W3C validator