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

Theorem tfinds2 7855
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 5306 . . . 4 ∅ ∈ V
3 tfinds2.1 . . . . 5 (𝑥 = ∅ → (𝜑𝜓))
43imbi2d 339 . . . 4 (𝑥 = ∅ → ((𝜏𝜑) ↔ (𝜏𝜓)))
52, 4sbcie 3819 . . 3 ([∅ / 𝑥](𝜏𝜑) ↔ (𝜏𝜓))
61, 5mpbir 230 . 2 [∅ / 𝑥](𝜏𝜑)
7 tfinds2.5 . . . . . . . 8 (𝑦 ∈ On → (𝜏 → (𝜒𝜃)))
87a2d 29 . . . . . . 7 (𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃)))
98sbcth 3791 . . . . . 6 (𝑥 ∈ V → [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))))
109elv 3478 . . . . 5 [𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃)))
11 sbcimg 3827 . . . . . 6 (𝑥 ∈ V → ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)))))
1211elv 3478 . . . . 5 ([𝑥 / 𝑦](𝑦 ∈ On → ((𝜏𝜒) → (𝜏𝜃))) ↔ ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃))))
1310, 12mpbi 229 . . . 4 ([𝑥 / 𝑦]𝑦 ∈ On → [𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)))
14 sbcel1v 3847 . . . 4 ([𝑥 / 𝑦]𝑦 ∈ On ↔ 𝑥 ∈ On)
15 sbcimg 3827 . . . . 5 (𝑥 ∈ V → ([𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)) ↔ ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃))))
1615elv 3478 . . . 4 ([𝑥 / 𝑦]((𝜏𝜒) → (𝜏𝜃)) ↔ ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃)))
1713, 14, 163imtr3i 290 . . 3 (𝑥 ∈ On → ([𝑥 / 𝑦](𝜏𝜒) → [𝑥 / 𝑦](𝜏𝜃)))
18 vex 3476 . . . 4 𝑥 ∈ V
19 tfinds2.2 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜒))
2019bicomd 222 . . . . . 6 (𝑥 = 𝑦 → (𝜒𝜑))
2120equcoms 2021 . . . . 5 (𝑦 = 𝑥 → (𝜒𝜑))
2221imbi2d 339 . . . 4 (𝑦 = 𝑥 → ((𝜏𝜒) ↔ (𝜏𝜑)))
2318, 22sbcie 3819 . . 3 ([𝑥 / 𝑦](𝜏𝜒) ↔ (𝜏𝜑))
24 vex 3476 . . . . . . 7 𝑦 ∈ V
2524sucex 7796 . . . . . 6 suc 𝑦 ∈ V
26 tfinds2.3 . . . . . . 7 (𝑥 = suc 𝑦 → (𝜑𝜃))
2726imbi2d 339 . . . . . 6 (𝑥 = suc 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜃)))
2825, 27sbcie 3819 . . . . 5 ([suc 𝑦 / 𝑥](𝜏𝜑) ↔ (𝜏𝜃))
2928sbcbii 3836 . . . 4 ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏𝜑) ↔ [𝑥 / 𝑦](𝜏𝜃))
30 suceq 6429 . . . . 5 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
3130sbcco2 3803 . . . 4 ([𝑥 / 𝑦][suc 𝑦 / 𝑥](𝜏𝜑) ↔ [suc 𝑥 / 𝑥](𝜏𝜑))
3229, 31bitr3i 276 . . 3 ([𝑥 / 𝑦](𝜏𝜃) ↔ [suc 𝑥 / 𝑥](𝜏𝜑))
3317, 23, 323imtr3g 294 . 2 (𝑥 ∈ On → ((𝜏𝜑) → [suc 𝑥 / 𝑥](𝜏𝜑)))
3419imbi2d 339 . . . . 5 (𝑥 = 𝑦 → ((𝜏𝜑) ↔ (𝜏𝜒)))
3534sbralie 3352 . . . 4 (∀𝑥𝑦 (𝜏𝜑) ↔ [𝑦 / 𝑥]∀𝑦𝑥 (𝜏𝜒))
36 sbsbc 3780 . . . 4 ([𝑦 / 𝑥]∀𝑦𝑥 (𝜏𝜒) ↔ [𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒))
3735, 36bitr2i 275 . . 3 ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) ↔ ∀𝑥𝑦 (𝜏𝜑))
38 r19.21v 3177 . . . . . . . 8 (∀𝑦𝑥 (𝜏𝜒) ↔ (𝜏 → ∀𝑦𝑥 𝜒))
39 tfinds2.6 . . . . . . . . 9 (Lim 𝑥 → (𝜏 → (∀𝑦𝑥 𝜒𝜑)))
4039a2d 29 . . . . . . . 8 (Lim 𝑥 → ((𝜏 → ∀𝑦𝑥 𝜒) → (𝜏𝜑)))
4138, 40biimtrid 241 . . . . . . 7 (Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
4241sbcth 3791 . . . . . 6 (𝑦 ∈ V → [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))))
4342elv 3478 . . . . 5 [𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
44 sbcimg 3827 . . . . . 6 (𝑦 ∈ V → ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))))
4544elv 3478 . . . . 5 ([𝑦 / 𝑥](Lim 𝑥 → (∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))) ↔ ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑))))
4643, 45mpbi 229 . . . 4 ([𝑦 / 𝑥]Lim 𝑥[𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)))
47 limeq 6375 . . . . 5 (𝑥 = 𝑦 → (Lim 𝑥 ↔ Lim 𝑦))
4824, 47sbcie 3819 . . . 4 ([𝑦 / 𝑥]Lim 𝑥 ↔ Lim 𝑦)
49 sbcimg 3827 . . . . 5 (𝑦 ∈ V → ([𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)) ↔ ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑))))
5049elv 3478 . . . 4 ([𝑦 / 𝑥](∀𝑦𝑥 (𝜏𝜒) → (𝜏𝜑)) ↔ ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑)))
5146, 48, 503imtr3i 290 . . 3 (Lim 𝑦 → ([𝑦 / 𝑥]𝑦𝑥 (𝜏𝜒) → [𝑦 / 𝑥](𝜏𝜑)))
5237, 51biimtrrid 242 . 2 (Lim 𝑦 → (∀𝑥𝑦 (𝜏𝜑) → [𝑦 / 𝑥](𝜏𝜑)))
536, 33, 52tfindes 7854 1 (𝑥 ∈ On → (𝜏𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  [wsb 2065  wcel 2104  wral 3059  Vcvv 3472  [wsbc 3776  c0 4321  Oncon0 6363  Lim wlim 6364  suc csuc 6365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369
This theorem is referenced by:  inar1  10772  grur1a  10816
  Copyright terms: Public domain W3C validator