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

Theorem tfindsg 7431
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 3914 . . . . . . 7 (𝑥 = ∅ → (𝐵𝑥𝐵 ⊆ ∅))
21adantl 482 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵𝑥𝐵 ⊆ ∅))
3 eqeq2 2806 . . . . . . . 8 (𝐵 = ∅ → (𝑥 = 𝐵𝑥 = ∅))
4 tfindsg.1 . . . . . . . 8 (𝑥 = 𝐵 → (𝜑𝜓))
53, 4syl6bir 255 . . . . . . 7 (𝐵 = ∅ → (𝑥 = ∅ → (𝜑𝜓)))
65imp 407 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑𝜓))
72, 6imbi12d 346 . . . . 5 ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
81imbi1d 343 . . . . . 6 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9 ss0 4272 . . . . . . . . 9 (𝐵 ⊆ ∅ → 𝐵 = ∅)
109con3i 157 . . . . . . . 8 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
1110pm2.21d 121 . . . . . . 7 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑𝜓)))
1211pm5.74d 274 . . . . . 6 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
138, 12sylan9bbr 511 . . . . 5 ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
147, 13pm2.61ian 808 . . . 4 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
1514imbi2d 342 . . 3 (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))))
16 sseq2 3914 . . . . 5 (𝑥 = 𝑦 → (𝐵𝑥𝐵𝑦))
17 tfindsg.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
1816, 17imbi12d 346 . . . 4 (𝑥 = 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵𝑦𝜒)))
1918imbi2d 342 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝑦𝜒))))
20 sseq2 3914 . . . . 5 (𝑥 = suc 𝑦 → (𝐵𝑥𝐵 ⊆ suc 𝑦))
21 tfindsg.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
2220, 21imbi12d 346 . . . 4 (𝑥 = suc 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ suc 𝑦𝜃)))
2322imbi2d 342 . . 3 (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦𝜃))))
24 sseq2 3914 . . . . 5 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
25 tfindsg.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
2624, 25imbi12d 346 . . . 4 (𝑥 = 𝐴 → ((𝐵𝑥𝜑) ↔ (𝐵𝐴𝜏)))
2726imbi2d 342 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝐴𝜏))))
28 tfindsg.5 . . . 4 (𝐵 ∈ On → 𝜓)
2928a1d 25 . . 3 (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))
30 vex 3440 . . . . . . . . . . . . . 14 𝑦 ∈ V
3130sucex 7382 . . . . . . . . . . . . 13 suc 𝑦 ∈ V
3231eqvinc 3581 . . . . . . . . . . . 12 (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵))
3328, 4syl5ibr 247 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑))
3421biimpd 230 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝜑𝜃))
3533, 34sylan9r 509 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3635exlimiv 1908 . . . . . . . . . . . 12 (∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3732, 36sylbi 218 . . . . . . . . . . 11 (suc 𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃))
3837eqcoms 2803 . . . . . . . . . 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 482 . . . . . 6 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
43 df-ne 2985 . . . . . . . . 9 (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
4443anbi2i 622 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45 annim 404 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
4644, 45bitri 276 . . . . . . 7 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
47 onsssuc 6153 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦𝐵 ∈ suc 𝑦))
48 suceloni 7384 . . . . . . . . . . 11 (𝑦 ∈ On → suc 𝑦 ∈ On)
49 onelpss 6106 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5048, 49sylan2 592 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5147, 50bitrd 280 . . . . . . . . 9 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5251ancoms 459 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
53 tfindsg.6 . . . . . . . . . . . 12 (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝑦) → (𝜒𝜃))
5453ex 413 . . . . . . . . . . 11 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → (𝜒𝜃)))
5554a1ddd 80 . . . . . . . . . 10 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦𝜃))))
5655a2d 29 . . . . . . . . 9 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵𝑦𝜒) → (𝐵𝑦 → (𝐵 ⊆ suc 𝑦𝜃))))
5756com23 86 . . . . . . . 8 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (𝐵𝑦 → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
5852, 57sylbird 261 . . . . . . 7 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
5946, 58syl5bir 244 . . . . . 6 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6042, 59pm2.61d 180 . . . . 5 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃)))
6160ex 413 . . . 4 (𝑦 ∈ On → (𝐵 ∈ On → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6261a2d 29 . . 3 (𝑦 ∈ On → ((𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦𝜃))))
63 pm2.27 42 . . . . . . . . 9 (𝐵 ∈ On → ((𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵𝑦𝜒)))
6463ralimdv 3145 . . . . . . . 8 (𝐵 ∈ On → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → ∀𝑦𝑥 (𝐵𝑦𝜒)))
6564ad2antlr 723 . . . . . . 7 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → ∀𝑦𝑥 (𝐵𝑦𝜒)))
66 tfindsg.7 . . . . . . 7 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵𝑦𝜒) → 𝜑))
6765, 66syld 47 . . . . . 6 (((Lim 𝑥𝐵 ∈ On) ∧ 𝐵𝑥) → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))
6867exp31 420 . . . . 5 (Lim 𝑥 → (𝐵 ∈ On → (𝐵𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))))
6968com3l 89 . . . 4 (𝐵 ∈ On → (𝐵𝑥 → (Lim 𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → 𝜑))))
7069com4t 93 . . 3 (Lim 𝑥 → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → (𝐵 ∈ On → (𝐵𝑥𝜑))))
7115, 19, 23, 27, 29, 62, 70tfinds 7430 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐵𝐴𝜏)))
7271imp31 418 1 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝐴) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1522  wex 1761  wcel 2081  wne 2984  wral 3105  wss 3859  c0 4211  Oncon0 6066  Lim wlim 6067  suc csuc 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-tr 5064  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072
This theorem is referenced by:  tfindsg2  7432  oaordi  8022  infensuc  8542  r1ordg  9053
  Copyright terms: Public domain W3C validator