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

Theorem finds2 7321
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 4981 . . . . . 6 ∅ ∈ V
3 finds2.1 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜓))
43imbi2d 331 . . . . . 6 (𝑥 = ∅ → ((𝜏𝜑) ↔ (𝜏𝜓)))
52, 4elab 3544 . . . . 5 (∅ ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜓))
61, 5mpbir 222 . . . 4 ∅ ∈ {𝑥 ∣ (𝜏𝜑)}
7 finds2.5 . . . . . . 7 (𝑦 ∈ ω → (𝜏 → (𝜒𝜃)))
87a2d 29 . . . . . 6 (𝑦 ∈ ω → ((𝜏𝜒) → (𝜏𝜃)))
9 vex 3393 . . . . . . 7 𝑦 ∈ V
10 finds2.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
1110imbi2d 331 . . . . . . 7 (𝑥 = 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜒)))
129, 11elab 3544 . . . . . 6 (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜒))
139sucex 7238 . . . . . . 7 suc 𝑦 ∈ V
14 finds2.3 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝜑𝜃))
1514imbi2d 331 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜃)))
1613, 15elab 3544 . . . . . 6 (suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜃))
178, 12, 163imtr4g 287 . . . . 5 (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)}))
1817rgen 3109 . . . 4 𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})
19 peano5 7316 . . . 4 ((∅ ∈ {𝑥 ∣ (𝜏𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏𝜑)})
206, 18, 19mp2an 675 . . 3 ω ⊆ {𝑥 ∣ (𝜏𝜑)}
2120sseli 3791 . 2 (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏𝜑)})
22 abid 2793 . 2 (𝑥 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜑))
2321, 22sylib 209 1 (𝑥 ∈ ω → (𝜏𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2158  {cab 2791  wral 3095  wss 3766  c0 4113  suc csuc 5935  ωcom 7292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-tr 4943  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-om 7293
This theorem is referenced by:  finds1  7322  onnseq  7674  nnacl  7925  nnmcl  7926  nnecl  7927  nnacom  7931  nnaass  7936  nndi  7937  nnmass  7938  nnmsucr  7939  nnmcom  7940  nnmordi  7945  omsmolem  7967  isinf  8409  unblem2  8449  fiint  8473  dffi3  8573  card2inf  8696  cantnfle  8812  cantnflt  8813  cantnflem1  8830  cnfcom  8841  trcl  8848  fseqenlem1  9127  infpssrlem3  9409  fin23lem26  9429  axdc3lem2  9555  axdc4lem  9559  axdclem2  9624  wunr1om  9823  wuncval2  9851  tskr1om  9871  grothomex  9933  peano5nni  11305  neibastop2lem  32673  finxpreclem6  33546
  Copyright terms: Public domain W3C validator