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

Theorem tfindsg 7707
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 3948 . . . . . . 7 (𝑥 = ∅ → (𝐵𝑥𝐵 ⊆ ∅))
21adantl 482 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵𝑥𝐵 ⊆ ∅))
3 eqeq2 2750 . . . . . . . 8 (𝐵 = ∅ → (𝑥 = 𝐵𝑥 = ∅))
4 tfindsg.1 . . . . . . . 8 (𝑥 = 𝐵 → (𝜑𝜓))
53, 4syl6bir 253 . . . . . . 7 (𝐵 = ∅ → (𝑥 = ∅ → (𝜑𝜓)))
65imp 407 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑𝜓))
72, 6imbi12d 345 . . . . 5 ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
81imbi1d 342 . . . . . 6 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9 ss0 4334 . . . . . . . . 9 (𝐵 ⊆ ∅ → 𝐵 = ∅)
109con3i 154 . . . . . . . 8 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
1110pm2.21d 121 . . . . . . 7 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑𝜓)))
1211pm5.74d 272 . . . . . 6 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
138, 12sylan9bbr 511 . . . . 5 ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
147, 13pm2.61ian 809 . . . 4 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
1514imbi2d 341 . . 3 (𝑥 = ∅ → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))))
16 sseq2 3948 . . . . 5 (𝑥 = 𝑦 → (𝐵𝑥𝐵𝑦))
17 tfindsg.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
1816, 17imbi12d 345 . . . 4 (𝑥 = 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵𝑦𝜒)))
1918imbi2d 341 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝑦𝜒))))
20 sseq2 3948 . . . . 5 (𝑥 = suc 𝑦 → (𝐵𝑥𝐵 ⊆ suc 𝑦))
21 tfindsg.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
2220, 21imbi12d 345 . . . 4 (𝑥 = suc 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ suc 𝑦𝜃)))
2322imbi2d 341 . . 3 (𝑥 = suc 𝑦 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵 ⊆ suc 𝑦𝜃))))
24 sseq2 3948 . . . . 5 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
25 tfindsg.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
2624, 25imbi12d 345 . . . 4 (𝑥 = 𝐴 → ((𝐵𝑥𝜑) ↔ (𝐵𝐴𝜏)))
2726imbi2d 341 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ On → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ On → (𝐵𝐴𝜏))))
28 tfindsg.5 . . . 4 (𝐵 ∈ On → 𝜓)
2928a1d 25 . . 3 (𝐵 ∈ On → (𝐵 ⊆ ∅ → 𝜓))
30 vex 3435 . . . . . . . . . . . . . 14 𝑦 ∈ V
3130sucex 7656 . . . . . . . . . . . . 13 suc 𝑦 ∈ V
3231eqvinc 3580 . . . . . . . . . . . 12 (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵))
3328, 4syl5ibr 245 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐵 ∈ On → 𝜑))
3421biimpd 228 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝜑𝜃))
3533, 34sylan9r 509 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3635exlimiv 1933 . . . . . . . . . . . 12 (∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ On → 𝜃))
3732, 36sylbi 216 . . . . . . . . . . 11 (suc 𝑦 = 𝐵 → (𝐵 ∈ On → 𝜃))
3837eqcoms 2746 . . . . . . . . . 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 2944 . . . . . . . . 9 (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
4443anbi2i 623 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45 annim 404 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
4644, 45bitri 274 . . . . . . 7 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
47 onsssuc 6355 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦𝐵 ∈ suc 𝑦))
48 suceloni 7659 . . . . . . . . . . 11 (𝑦 ∈ On → suc 𝑦 ∈ On)
49 onelpss 6308 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5048, 49sylan2 593 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5147, 50bitrd 278 . . . . . . . . 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 259 . . . . . . 7 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
5946, 58syl5bir 242 . . . . . 6 ((𝑦 ∈ On ∧ 𝐵 ∈ On) → (¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6042, 59pm2.61d 179 . . . . 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 3109 . . . . . . . 8 (𝐵 ∈ On → (∀𝑦𝑥 (𝐵 ∈ On → (𝐵𝑦𝜒)) → ∀𝑦𝑥 (𝐵𝑦𝜒)))
6564ad2antlr 724 . . . . . . 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 7706 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (𝐵𝐴𝜏)))
7271imp31 418 1 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵𝐴) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  wne 2943  wral 3064  wss 3888  c0 4258  Oncon0 6268  Lim wlim 6269  suc csuc 6270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pr 5354  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-opab 5139  df-tr 5194  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-ord 6271  df-on 6272  df-lim 6273  df-suc 6274
This theorem is referenced by:  tfindsg2  7708  oaordi  8375  infensuc  8940  r1ordg  9534
  Copyright terms: Public domain W3C validator