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

Theorem tfinds2 7792
Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff 𝜏 is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
tfinds2.1 (𝑥 = ∅ → (𝜑𝜓))
tfinds2.2 (𝑥 = 𝑦 → (𝜑𝜒))
tfinds2.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
tfinds2.4 (𝜏𝜓)
tfinds2.5 (𝑦 ∈ On → (𝜏 → (𝜒𝜃)))
tfinds2.6 (Lim 𝑥 → (𝜏 → (∀𝑦𝑥 𝜒𝜑)))
Assertion
Ref Expression
tfinds2 (𝑥 ∈ On → (𝜏𝜑))
Distinct variable groups:   𝑥,𝑦,𝜏   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)

Proof of Theorem tfinds2
StepHypRef Expression
1 tfinds2.4 . . 3 (𝜏𝜓)
2 0ex 5262 . . . 4 ∅ ∈ V
3 tfinds2.1 . . . . 5 (𝑥 = ∅ → (𝜑𝜓))
43imbi2d 340 . . . 4 (𝑥 = ∅ → ((𝜏𝜑) ↔ (𝜏𝜓)))
52, 4sbcie 3780 . . 3 ([∅ / 𝑥](𝜏𝜑) ↔ (𝜏𝜓))
61, 5mpbir 230 . 2 [∅ / 𝑥](𝜏𝜑)
7 tfinds2.5 . . . . . . . 8 (𝑦 ∈ On → (𝜏 → (𝜒𝜃)))
87a2d 29 . . . . . . 7 (𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃)))
98sbcth 3752 . . . . . 6 (𝑥 ∈ V → [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))))
109elv 3449 . . . . 5 [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃)))
11 sbcimg 3788 . . . . . 6 (𝑥 ∈ V → ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)))))
1211elv 3449 . . . . 5 ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃))))
1310, 12mpbi 229 . . . 4 ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)))
14 sbcel1v 3808 . . . 4 ([𝑥 / 𝑦]𝑦 ∈ On ↔ 𝑥 ∈ On)
15 sbcimg 3788 . . . . 5 (𝑥 ∈ V → ([𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)) ↔ ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃))))
1615elv 3449 . . . 4 ([𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)) ↔ ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃)))
1713, 14, 163imtr3i 290 . . 3 (𝑥 ∈ On → ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃)))
18 vex 3447 . . . 4 𝑥 ∈ V
19 tfinds2.2 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜒))
2019bicomd 222 . . . . . 6 (𝑥 = 𝑦 → (𝜒𝜑))
2120equcoms 2023 . . . . 5 (𝑦 = 𝑥 → (𝜒𝜑))
2221imbi2d 340 . . . 4 (𝑦 = 𝑥 → ((𝜏𝜒) ↔ (𝜏𝜑)))
2318, 22sbcie 3780 . . 3 ([𝑥 / 𝑦](𝜏𝜒) ↔ (𝜏𝜑))
24 vex 3447 . . . . . . 7 𝑦 ∈ V
2524sucex 7733 . . . . . 6 suc 𝑦 ∈ V
26 tfinds2.3 . . . . . . 7 (𝑥 = suc 𝑦 → (𝜑𝜃))
2726imbi2d 340 . . . . . 6 (𝑥 = suc 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜃)))
2825, 27sbcie 3780 . . . . 5 ([suc 𝑦 / 𝑥](𝜏𝜑) ↔ (𝜏𝜃))
2928sbcbii 3797 . . . 4 ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏𝜑) ↔ [𝑥 / 𝑦](𝜏𝜃))
30 suceq 6381 . . . . 5 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
3130sbcco2 3764 . . . 4 ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏𝜑) ↔ [suc 𝑥 / 𝑥](𝜏𝜑))
3229, 31bitr3i 276 . . 3 ([𝑥 / 𝑦](𝜏𝜃) ↔ [suc 𝑥 / 𝑥](𝜏𝜑))
3317, 23, 323imtr3g 294 . 2 (𝑥 ∈ On → ((𝜏𝜑) → [suc 𝑥 / 𝑥](𝜏𝜑)))
3419imbi2d 340 . . . . 5 (𝑥 = 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜒)))
3534sbralie 3330 . . . 4 (∀𝑥𝑦 (𝜏𝜑) ↔ [𝑦 / 𝑥]∀𝑦𝑥 (𝜏𝜒))
36 sbsbc 3741 . . . 4 ([𝑦 / 𝑥]∀𝑦𝑥 (𝜏𝜒) ↔ [𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒))
3735, 36bitr2i 275 . . 3 ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) ↔ ∀𝑥𝑦 (𝜏𝜑))
38 r19.21v 3174 . . . . . . . 8 (∀𝑦𝑥 (𝜏𝜒) ↔ (𝜏 → ∀𝑦𝑥 𝜒))
39 tfinds2.6 . . . . . . . . 9 (Lim 𝑥 → (𝜏 → (∀𝑦𝑥 𝜒𝜑)))
4039a2d 29 . . . . . . . 8 (Lim 𝑥 → ((𝜏 → ∀𝑦𝑥 𝜒) → (𝜏𝜑)))
4138, 40biimtrid 241 . . . . . . 7 (Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
4241sbcth 3752 . . . . . 6 (𝑦 ∈ V → [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))))
4342elv 3449 . . . . 5 [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
44 sbcimg 3788 . . . . . 6 (𝑦 ∈ V → ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))))
4544elv 3449 . . . . 5 ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))))
4643, 45mpbi 229 . . . 4 ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
47 limeq 6327 . . . . 5 (𝑥 = 𝑦 → (Lim 𝑥 ↔ Lim 𝑦))
4824, 47sbcie 3780 . . . 4 ([𝑦 / 𝑥]Lim 𝑥 ↔ Lim 𝑦)
49 sbcimg 3788 . . . . 5 (𝑦 ∈ V → ([𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)) ↔ ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑))))
5049elv 3449 . . . 4 ([𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)) ↔ ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑)))
5146, 48, 503imtr3i 290 . . 3 (Lim 𝑦 → ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑)))
5237, 51biimtrrid 242 . 2 (Lim 𝑦 → (∀𝑥𝑦 (𝜏𝜑) → [𝑦 / 𝑥](𝜏𝜑)))
536, 33, 52tfindes 7791 1 (𝑥 ∈ On → (𝜏𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  [wsb 2067  wcel 2106  wral 3062  Vcvv 3443  [wsbc 3737  c0 4280  Oncon0 6315  Lim wlim 6316  suc csuc 6317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-tr 5221  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321
This theorem is referenced by:  inar1  10669  grur1a  10713
  Copyright terms: Public domain W3C validator