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

Theorem finds2 7838
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 5265 . . . . . 6 ∅ ∈ V
3 finds2.1 . . . . . . 7 (𝑥 = ∅ → (𝜑𝜓))
43imbi2d 341 . . . . . 6 (𝑥 = ∅ → ((𝜏𝜑) ↔ (𝜏𝜓)))
52, 4elab 3631 . . . . 5 (∅ ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜓))
61, 5mpbir 230 . . . 4 ∅ ∈ {𝑥 ∣ (𝜏𝜑)}
7 finds2.5 . . . . . . 7 (𝑦 ∈ ω → (𝜏 → (𝜒𝜃)))
87a2d 29 . . . . . 6 (𝑦 ∈ ω → ((𝜏𝜒) → (𝜏𝜃)))
9 vex 3448 . . . . . . 7 𝑦 ∈ V
10 finds2.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
1110imbi2d 341 . . . . . . 7 (𝑥 = 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜒)))
129, 11elab 3631 . . . . . 6 (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜒))
139sucex 7742 . . . . . . 7 suc 𝑦 ∈ V
14 finds2.3 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝜑𝜃))
1514imbi2d 341 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜃)))
1613, 15elab 3631 . . . . . 6 (suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜃))
178, 12, 163imtr4g 296 . . . . 5 (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)}))
1817rgen 3063 . . . 4 𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})
19 peano5 7831 . . . 4 ((∅ ∈ {𝑥 ∣ (𝜏𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏𝜑)})
206, 18, 19mp2an 691 . . 3 ω ⊆ {𝑥 ∣ (𝜏𝜑)}
2120sseli 3941 . 2 (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏𝜑)})
22 abid 2714 . 2 (𝑥 ∈ {𝑥 ∣ (𝜏𝜑)} ↔ (𝜏𝜑))
2321, 22sylib 217 1 (𝑥 ∈ ω → (𝜏𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  {cab 2710  wral 3061  wss 3911  c0 4283  suc csuc 6320  ωcom 7803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-tr 5224  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-om 7804
This theorem is referenced by:  finds1  7839  onnseq  8291  nnacl  8559  nnmcl  8560  nnecl  8561  nnacom  8565  nnaass  8570  nndi  8571  nnmass  8572  nnmsucr  8573  nnmcom  8574  nnmordi  8579  omsmolem  8604  isinf  9207  isinfOLD  9208  unblem2  9243  fiint  9271  dffi3  9372  card2inf  9496  cantnfle  9612  cantnflt  9613  cantnflem1  9630  cnfcom  9641  trcl  9669  fseqenlem1  9965  nnadju  10138  infpssrlem3  10246  fin23lem26  10266  axdc3lem2  10392  axdc4lem  10396  axdclem2  10461  wunr1om  10660  wuncval2  10688  tskr1om  10708  grothomex  10770  peano5nni  12161  neibastop2lem  34878  finxpreclem6  35913  domalom  35921  oaabsb  41672
  Copyright terms: Public domain W3C validator