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

Theorem tfindsg2 7009
Description: 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. The basis of this version is an arbitrary ordinal suc 𝐵 instead of zero. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 5-Jan-2005.)
Hypotheses
Ref Expression
tfindsg2.1 (𝑥 = suc 𝐵 → (𝜑𝜓))
tfindsg2.2 (𝑥 = 𝑦 → (𝜑𝜒))
tfindsg2.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
tfindsg2.4 (𝑥 = 𝐴 → (𝜑𝜏))
tfindsg2.5 (𝐵 ∈ On → 𝜓)
tfindsg2.6 ((𝑦 ∈ On ∧ 𝐵𝑦) → (𝜒𝜃))
tfindsg2.7 ((Lim 𝑥𝐵𝑥) → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑))
Assertion
Ref Expression
tfindsg2 ((𝐴 ∈ On ∧ 𝐵𝐴) → 𝜏)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem tfindsg2
StepHypRef Expression
1 onelon 5710 . . 3 ((𝐴 ∈ On ∧ 𝐵𝐴) → 𝐵 ∈ On)
2 sucelon 6965 . . 3 (𝐵 ∈ On ↔ suc 𝐵 ∈ On)
31, 2sylib 208 . 2 ((𝐴 ∈ On ∧ 𝐵𝐴) → suc 𝐵 ∈ On)
4 eloni 5695 . . . 4 (𝐴 ∈ On → Ord 𝐴)
5 ordsucss 6966 . . . 4 (Ord 𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
64, 5syl 17 . . 3 (𝐴 ∈ On → (𝐵𝐴 → suc 𝐵𝐴))
76imp 445 . 2 ((𝐴 ∈ On ∧ 𝐵𝐴) → suc 𝐵𝐴)
8 tfindsg2.1 . . . . 5 (𝑥 = suc 𝐵 → (𝜑𝜓))
9 tfindsg2.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
10 tfindsg2.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
11 tfindsg2.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
12 tfindsg2.5 . . . . . 6 (𝐵 ∈ On → 𝜓)
132, 12sylbir 225 . . . . 5 (suc 𝐵 ∈ On → 𝜓)
14 eloni 5695 . . . . . . . . . 10 (𝑦 ∈ On → Ord 𝑦)
15 ordelsuc 6968 . . . . . . . . . 10 ((𝐵 ∈ On ∧ Ord 𝑦) → (𝐵𝑦 ↔ suc 𝐵𝑦))
1614, 15sylan2 491 . . . . . . . . 9 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦 ↔ suc 𝐵𝑦))
1716ancoms 469 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 ↔ suc 𝐵𝑦))
18 tfindsg2.6 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝐵𝑦) → (𝜒𝜃))
1918ex 450 . . . . . . . . 9 (𝑦 ∈ On → (𝐵𝑦 → (𝜒𝜃)))
2019adantr 481 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → (𝜒𝜃)))
2117, 20sylbird 250 . . . . . . 7 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (suc 𝐵𝑦 → (𝜒𝜃)))
222, 21sylan2br 493 . . . . . 6 ((𝑦 ∈ On ∧ suc 𝐵 ∈ On) → (suc 𝐵𝑦 → (𝜒𝜃)))
2322imp 445 . . . . 5 (((𝑦 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵𝑦) → (𝜒𝜃))
24 tfindsg2.7 . . . . . . . . . 10 ((Lim 𝑥𝐵𝑥) → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑))
2524ex 450 . . . . . . . . 9 (Lim 𝑥 → (𝐵𝑥 → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑)))
2625adantr 481 . . . . . . . 8 ((Lim 𝑥𝐵 ∈ On) → (𝐵𝑥 → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑)))
27 vex 3194 . . . . . . . . . . 11 𝑥 ∈ V
28 limelon 5750 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
2927, 28mpan 705 . . . . . . . . . 10 (Lim 𝑥𝑥 ∈ On)
30 eloni 5695 . . . . . . . . . . . 12 (𝑥 ∈ On → Ord 𝑥)
31 ordelsuc 6968 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ Ord 𝑥) → (𝐵𝑥 ↔ suc 𝐵𝑥))
3230, 31sylan2 491 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵𝑥 ↔ suc 𝐵𝑥))
33 onelon 5710 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
3433, 14syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑦𝑥) → Ord 𝑦)
3534, 15sylan2 491 . . . . . . . . . . . . . . 15 ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦𝑥)) → (𝐵𝑦 ↔ suc 𝐵𝑦))
3635anassrs 679 . . . . . . . . . . . . . 14 (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦𝑥) → (𝐵𝑦 ↔ suc 𝐵𝑦))
3736imbi1d 331 . . . . . . . . . . . . 13 (((𝐵 ∈ On ∧ 𝑥 ∈ On) ∧ 𝑦𝑥) → ((𝐵𝑦𝜒) ↔ (suc 𝐵𝑦𝜒)))
3837ralbidva 2984 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐵𝑦𝜒) ↔ ∀𝑦𝑥 (suc 𝐵𝑦𝜒)))
3938imbi1d 331 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑) ↔ (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑)))
4032, 39imbi12d 334 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((𝐵𝑥 → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑)) ↔ (suc 𝐵𝑥 → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑))))
4129, 40sylan2 491 . . . . . . . . 9 ((𝐵 ∈ On ∧ Lim 𝑥) → ((𝐵𝑥 → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑)) ↔ (suc 𝐵𝑥 → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑))))
4241ancoms 469 . . . . . . . 8 ((Lim 𝑥𝐵 ∈ On) → ((𝐵𝑥 → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑)) ↔ (suc 𝐵𝑥 → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑))))
4326, 42mpbid 222 . . . . . . 7 ((Lim 𝑥𝐵 ∈ On) → (suc 𝐵𝑥 → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑)))
442, 43sylan2br 493 . . . . . 6 ((Lim 𝑥 ∧ suc 𝐵 ∈ On) → (suc 𝐵𝑥 → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑)))
4544imp 445 . . . . 5 (((Lim 𝑥 ∧ suc 𝐵 ∈ On) ∧ suc 𝐵𝑥) → (∀𝑦𝑥 (suc 𝐵𝑦𝜒) → 𝜑))
468, 9, 10, 11, 13, 23, 45tfindsg 7008 . . . 4 (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ suc 𝐵𝐴) → 𝜏)
4746expl 647 . . 3 (𝐴 ∈ On → ((suc 𝐵 ∈ On ∧ suc 𝐵𝐴) → 𝜏))
4847adantr 481 . 2 ((𝐴 ∈ On ∧ 𝐵𝐴) → ((suc 𝐵 ∈ On ∧ suc 𝐵𝐴) → 𝜏))
493, 7, 48mp2and 714 1 ((𝐴 ∈ On ∧ 𝐵𝐴) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wral 2912  Vcvv 3191  wss 3560  Ord word 5684  Oncon0 5685  Lim wlim 5686  suc csuc 5687
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 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903
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 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691
This theorem is referenced by:  oeordi  7613
  Copyright terms: Public domain W3C validator