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

Theorem tfinds 6951
 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 6939 . . . . 5 (Lim 𝑥 ↔ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
43notbii 309 . . . 4 (¬ Lim 𝑥 ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
5 iman 439 . . . . 5 ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) ↔ ¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)))
6 eloni 5650 . . . . . . 7 (𝑥 ∈ On → Ord 𝑥)
7 pm2.27 41 . . . . . . 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 247 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1211a1d 25 . . . . . . 7 (𝑥 = ∅ → (∀𝑦𝑥 𝜒𝜑))
13 nfra1 2925 . . . . . . . . 9 𝑦𝑦𝑥 𝜒
14 nfv 1830 . . . . . . . . 9 𝑦𝜑
1513, 14nfim 1813 . . . . . . . 8 𝑦(∀𝑦𝑥 𝜒𝜑)
16 vex 3176 . . . . . . . . . . . . 13 𝑦 ∈ V
1716sucid 5721 . . . . . . . . . . . 12 𝑦 ∈ suc 𝑦
181rspcv 3278 . . . . . . . . . . . 12 (𝑦 ∈ suc 𝑦 → (∀𝑥 ∈ suc 𝑦𝜑𝜒))
1917, 18ax-mp 5 . . . . . . . . . . 11 (∀𝑥 ∈ suc 𝑦𝜑𝜒)
20 tfinds.6 . . . . . . . . . . 11 (𝑦 ∈ On → (𝜒𝜃))
2119, 20syl5 33 . . . . . . . . . 10 (𝑦 ∈ On → (∀𝑥 ∈ suc 𝑦𝜑𝜃))
22 raleq 3115 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (∀𝑧𝑥 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑))
23 nfv 1830 . . . . . . . . . . . . . . 15 𝑥𝜒
2423, 1sbie 2396 . . . . . . . . . . . . . 14 ([𝑦 / 𝑥]𝜑𝜒)
25 sbequ 2364 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
2624, 25syl5bbr 273 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝜒 ↔ [𝑧 / 𝑥]𝜑))
2726cbvralv 3147 . . . . . . . . . . . 12 (∀𝑦𝑥 𝜒 ↔ ∀𝑧𝑥 [𝑧 / 𝑥]𝜑)
28 cbvralsv 3158 . . . . . . . . . . . 12 (∀𝑥 ∈ suc 𝑦𝜑 ↔ ∀𝑧 ∈ suc 𝑦[𝑧 / 𝑥]𝜑)
2922, 27, 283bitr4g 302 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒 ↔ ∀𝑥 ∈ suc 𝑦𝜑))
3029imbi1d 330 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((∀𝑦𝑥 𝜒𝜃) ↔ (∀𝑥 ∈ suc 𝑦𝜑𝜃)))
3121, 30syl5ibrcom 236 . . . . . . . . 9 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜃)))
32 tfinds.3 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝜑𝜃))
3332biimprd 237 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝜃𝜑))
3433a1i 11 . . . . . . . . 9 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (𝜃𝜑)))
3531, 34syldd 70 . . . . . . . 8 (𝑦 ∈ On → (𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜑)))
3615, 35rexlimi 3006 . . . . . . 7 (∃𝑦 ∈ On 𝑥 = suc 𝑦 → (∀𝑦𝑥 𝜒𝜑))
3712, 36jaoi 393 . . . . . 6 ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦) → (∀𝑦𝑥 𝜒𝜑))
388, 37syl6 34 . . . . 5 (𝑥 ∈ On → ((Ord 𝑥 → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦𝑥 𝜒𝜑)))
395, 38syl5bir 232 . . . 4 (𝑥 ∈ On → (¬ (Ord 𝑥 ∧ ¬ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦)) → (∀𝑦𝑥 𝜒𝜑)))
404, 39syl5bi 231 . . 3 (𝑥 ∈ On → (¬ Lim 𝑥 → (∀𝑦𝑥 𝜒𝜑)))
41 tfinds.7 . . 3 (Lim 𝑥 → (∀𝑦𝑥 𝜒𝜑))
4240, 41pm2.61d2 171 . 2 (𝑥 ∈ On → (∀𝑦𝑥 𝜒𝜑))
431, 2, 42tfis3 6949 1 (𝐴 ∈ On → 𝜏)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475  [wsb 1867   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ∅c0 3874  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646 This theorem is referenced by:  tfindsg  6952  tfindes  6954  tfinds3  6956  oa0r  7505  om0r  7506  om1r  7510  oe1m  7512  oeoalem  7563  r1sdom  8520  r1tr  8522  alephon  8775  alephcard  8776  alephordi  8780  rdgprc  30944
 Copyright terms: Public domain W3C validator