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

Theorem tfinds 7021
Description: Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 16-Apr-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypotheses
Ref Expression
tfinds.1 (𝑥 = ∅ → (𝜑𝜓))
tfinds.2 (𝑥 = 𝑦 → (𝜑𝜒))
tfinds.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
tfinds.4 (𝑥 = 𝐴 → (𝜑𝜏))
tfinds.5 𝜓
tfinds.6 (𝑦 ∈ On → (𝜒𝜃))
tfinds.7 (Lim 𝑥 → (∀𝑦𝑥 𝜒𝜑))
Assertion
Ref Expression
tfinds (𝐴 ∈ On → 𝜏)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜒,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝜒(𝑦)   𝜃(𝑥,𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem tfinds
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 tfinds.2 . 2 (𝑥 = 𝑦 → (𝜑𝜒))
2 tfinds.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
3 dflim3 7009 . . . . 5 (Lim 𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
43notbii 310 . . . 4 (¬ Lim 𝑥 ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
5 iman 440 . . . . 5 ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
6 eloni 5702 . . . . . . 7 (𝑥 ∈ On → Ord 𝑥)
7 pm2.27 42 . . . . . . 7 (Ord 𝑥 → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
86, 7syl 17 . . . . . 6 (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
9 tfinds.5 . . . . . . . . 9 𝜓
10 tfinds.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
119, 10mpbiri 248 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1211a1d 25 . . . . . . 7 (𝑥 = ∅ → (∀𝑦𝑥 𝜒𝜑))
13 nfra1 2937 . . . . . . . . 9 𝑦𝑦𝑥 𝜒
14 nfv 1840 . . . . . . . . 9 𝑦𝜑
1513, 14nfim 1822 . . . . . . . 8 𝑦(∀𝑦𝑥 𝜒𝜑)
16 vex 3193 . . . . . . . . . . . . 13 𝑦 ∈ V
1716sucid 5773 . . . . . . . . . . . 12 𝑦 ∈ suc 𝑦
181rspcv 3295 . . . . . . . . . . . 12 (𝑦 ∈ suc 𝑦 → (∀𝑥 ∈ suc 𝑦𝜑𝜒))
1917, 18ax-mp 5 . . . . . . . . . . 11 (∀𝑥 ∈ suc 𝑦𝜑𝜒)
20 tfinds.6 . . . . . . . . . . 11 (𝑦 ∈ On → (𝜒𝜃))
2119, 20syl5 34 . . . . . . . . . 10 (𝑦 ∈ On → (∀𝑥 ∈ suc 𝑦𝜑𝜃))
22 raleq 3131 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (∀𝑧𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23 nfv 1840 . . . . . . . . . . . . . . 15 𝑥𝜒
2423, 1sbie 2407 . . . . . . . . . . . . . 14 ([𝑦 / 𝑥]𝜑𝜒)
25 sbequ 2375 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
2624, 25syl5bbr 274 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
2726cbvralv 3163 . . . . . . . . . . . 12 (∀𝑦𝑥 𝜒 ↔ ∀𝑧𝑥 [𝑧 / 𝑥]𝜑)
28 cbvralsv 3174 . . . . . . . . . . . 12 (∀𝑥 ∈ suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)
2922, 27, 283bitr4g 303 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑))
3029imbi1d 331 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((∀𝑦𝑥 𝜒𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑𝜃)))
3121, 30syl5ibrcom 237 . . . . . . . . 9 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜃)))
32 tfinds.3 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝜑𝜃))
3332biimprd 238 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝜃𝜑))
3433a1i 11 . . . . . . . . 9 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃𝜑)))
3531, 34syldd 72 . . . . . . . 8 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜑)))
3615, 35rexlimi 3019 . . . . . . 7 (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜑))
3712, 36jaoi 394 . . . . . 6 ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦𝑥 𝜒𝜑))
388, 37syl6 35 . . . . 5 (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦𝑥 𝜒𝜑)))
395, 38syl5bir 233 . . . 4 (𝑥 ∈ On → (¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦𝑥 𝜒𝜑)))
404, 39syl5bi 232 . . 3 (𝑥 ∈ On → (¬ Lim 𝑥 → (∀𝑦𝑥 𝜒𝜑)))
41 tfinds.7 . . 3 (Lim 𝑥 → (∀𝑦𝑥 𝜒𝜑))
4240, 41pm2.61d2 172 . 2 (𝑥 ∈ On → (∀𝑦𝑥 𝜒𝜑))
431, 2, 42tfis3 7019 1 (𝐴 ∈ On → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  [wsb 1877  wcel 1987  wral 2908  wrex 2909  c0 3897  Ord word 5691  Oncon0 5692  Lim wlim 5693  suc csuc 5694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698
This theorem is referenced by:  tfindsg  7022  tfindes  7024  tfinds3  7026  oa0r  7578  om0r  7579  om1r  7583  oe1m  7585  oeoalem  7636  r1sdom  8597  r1tr  8599  alephon  8852  alephcard  8853  alephordi  8857  rdgprc  31454
  Copyright terms: Public domain W3C validator