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

Theorem tfindsg 7286
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 𝐵 instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.)
Hypotheses
Ref Expression
tfindsg.1 (𝑥 = 𝐵 → (𝜑𝜓))
tfindsg.2 (𝑥 = 𝑦 → (𝜑𝜒))
tfindsg.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
tfindsg.4 (𝑥 = 𝐴 → (𝜑𝜏))
tfindsg.5 (𝐵 ∈ On → 𝜓)
tfindsg.6 (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝑦) → (𝜒𝜃))
tfindsg.7 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑))
Assertion
Ref Expression
tfindsg (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝐴) → 𝜏)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem tfindsg
StepHypRef Expression
1 sseq2 3824 . . . . . . 7 (𝑥 = ∅ → (𝐵𝑥𝐵 ⊆ ∅))
21adantl 469 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵𝑥𝐵 ⊆ ∅))
3 eqeq2 2817 . . . . . . . 8 (𝐵 = ∅ → (𝑥 = 𝐵𝑥 = ∅))
4 tfindsg.1 . . . . . . . 8 (𝑥 = 𝐵 → (𝜑𝜓))
53, 4syl6bir 245 . . . . . . 7 (𝐵 = ∅ → (𝑥 = ∅ → (𝜑𝜓)))
65imp 395 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑𝜓))
72, 6imbi12d 335 . . . . 5 ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
81imbi1d 332 . . . . . 6 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9 ss0 4172 . . . . . . . . 9 (𝐵 ⊆ ∅ → 𝐵 = ∅)
109con3i 151 . . . . . . . 8 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
1110pm2.21d 119 . . . . . . 7 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑𝜓)))
1211pm5.74d 264 . . . . . 6 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
138, 12sylan9bbr 502 . . . . 5 ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
147, 13pm2.61ian 837 . . . 4 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
1514imbi2d 331 . . 3 (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))))
16 sseq2 3824 . . . . 5 (𝑥 = 𝑦 → (𝐵𝑥𝐵𝑦))
17 tfindsg.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
1816, 17imbi12d 335 . . . 4 (𝑥 = 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵𝑦𝜒)))
1918imbi2d 331 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝑦𝜒))))
20 sseq2 3824 . . . . 5 (𝑥 = suc 𝑦 → (𝐵𝑥𝐵 ⊆ suc 𝑦))
21 tfindsg.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
2220, 21imbi12d 335 . . . 4 (𝑥 = suc 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ suc 𝑦𝜃)))
2322imbi2d 331 . . 3 (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦𝜃))))
24 sseq2 3824 . . . . 5 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
25 tfindsg.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
2624, 25imbi12d 335 . . . 4 (𝑥 = 𝐴 → ((𝐵𝑥𝜑) ↔ (𝐵𝐴𝜏)))
2726imbi2d 331 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝐴𝜏))))
28 tfindsg.5 . . . 4 (𝐵 ∈ On → 𝜓)
2928a1d 25 . . 3 (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))
30 vex 3394 . . . . . . . . . . . . . 14 𝑦 ∈ V
3130sucex 7237 . . . . . . . . . . . . 13 suc 𝑦 ∈ V
3231eqvinc 3524 . . . . . . . . . . . 12 (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵))
3328, 4syl5ibr 237 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑))
3421biimpd 220 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝜑𝜃))
3533, 34sylan9r 500 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3635exlimiv 2021 . . . . . . . . . . . 12 (∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3732, 36sylbi 208 . . . . . . . . . . 11 (suc 𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃))
3837eqcoms 2814 . . . . . . . . . 10 (𝐵 = suc 𝑦 → (𝐵 ∈ On → 𝜃))
3938imim2i 16 . . . . . . . . 9 ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃)))
4039a1d 25 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ On → 𝜃))))
4140com4r 94 . . . . . . 7 (𝐵 ∈ On → ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
4241adantl 469 . . . . . 6 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
43 df-ne 2979 . . . . . . . . 9 (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
4443anbi2i 611 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45 annim 392 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
4644, 45bitri 266 . . . . . . 7 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
47 onsssuc 6024 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦𝐵 ∈ suc 𝑦))
48 suceloni 7239 . . . . . . . . . . 11 (𝑦 ∈ On → suc 𝑦 ∈ On)
49 onelpss 5976 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5048, 49sylan2 582 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5147, 50bitrd 270 . . . . . . . . 9 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5251ancoms 448 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
53 tfindsg.6 . . . . . . . . . . . 12 (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝑦) → (𝜒𝜃))
5453ex 399 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → (𝜒𝜃)))
55 ax-1 6 . . . . . . . . . . 11 (𝜃 → (𝐵 ⊆ suc 𝑦𝜃))
5654, 55syl8 76 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦𝜃))))
5756a2d 29 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵𝑦𝜒) → (𝐵𝑦 → (𝐵 ⊆ suc 𝑦𝜃))))
5857com23 86 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
5952, 58sylbird 251 . . . . . . 7 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6046, 59syl5bir 234 . . . . . 6 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6142, 60pm2.61d 171 . . . . 5 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃)))
6261ex 399 . . . 4 (𝑦 ∈ On → (𝐵 ∈ On → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6362a2d 29 . . 3 (𝑦 ∈ On → ((𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦𝜃))))
64 pm2.27 42 . . . . . . . . 9 (𝐵 ∈ On → ((𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵𝑦𝜒)))
6564ralimdv 3151 . . . . . . . 8 (𝐵 ∈ On → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → ∀𝑦𝑥 (𝐵𝑦𝜒)))
6665ad2antlr 709 . . . . . . 7 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → ∀𝑦𝑥 (𝐵𝑦𝜒)))
67 tfindsg.7 . . . . . . 7 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑))
6866, 67syld 47 . . . . . 6 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))
6968exp31 408 . . . . 5 (Lim 𝑥 → (𝐵 ∈ On → (𝐵𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))))
7069com3l 89 . . . 4 (𝐵 ∈ On → (𝐵𝑥 → (Lim 𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))))
7170com4t 93 . . 3 (Lim 𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵 ∈ On → (𝐵𝑥𝜑))))
7215, 19, 23, 27, 29, 63, 71tfinds 7285 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐵𝐴𝜏)))
7372imp31 406 1 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝐴) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2156  wne 2978  wral 3096  wss 3769  c0 4116  Oncon0 5936  Lim wlim 5937  suc csuc 5938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096  ax-un 7175
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 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-tr 4947  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942
This theorem is referenced by:  tfindsg2  7287  oaordi  7859  infensuc  8373  r1ordg  8884
  Copyright terms: Public domain W3C validator