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

Theorem tfindes 6829
Description: Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.)
Hypotheses
Ref Expression
tfindes.1 [∅ / 𝑥]𝜑
tfindes.2 (𝑥 ∈ On → (𝜑[suc 𝑥 / 𝑥]𝜑))
tfindes.3 (Lim 𝑦 → (∀𝑥𝑦 𝜑[𝑦 / 𝑥]𝜑))
Assertion
Ref Expression
tfindes (𝑥 ∈ On → 𝜑)
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem tfindes
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 3308 . 2 (𝑦 = ∅ → ([𝑦 / 𝑥]𝜑[∅ / 𝑥]𝜑))
2 dfsbcq 3308 . 2 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑[𝑧 / 𝑥]𝜑))
3 dfsbcq 3308 . 2 (𝑦 = suc 𝑧 → ([𝑦 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑))
4 sbceq2a 3318 . 2 (𝑦 = 𝑥 → ([𝑦 / 𝑥]𝜑𝜑))
5 tfindes.1 . 2 [∅ / 𝑥]𝜑
6 nfv 1796 . . . 4 𝑥 𝑧 ∈ On
7 nfsbc1v 3326 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
8 nfsbc1v 3326 . . . . 5 𝑥[suc 𝑧 / 𝑥]𝜑
97, 8nfim 2051 . . . 4 𝑥([𝑧 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑)
106, 9nfim 2051 . . 3 𝑥(𝑧 ∈ On → ([𝑧 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑))
11 eleq1 2580 . . . 4 (𝑥 = 𝑧 → (𝑥 ∈ On ↔ 𝑧 ∈ On))
12 sbceq1a 3317 . . . . 5 (𝑥 = 𝑧 → (𝜑[𝑧 / 𝑥]𝜑))
13 suceq 5595 . . . . . 6 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
1413sbceq1d 3311 . . . . 5 (𝑥 = 𝑧 → ([suc 𝑥 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑))
1512, 14imbi12d 332 . . . 4 (𝑥 = 𝑧 → ((𝜑[suc 𝑥 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑)))
1611, 15imbi12d 332 . . 3 (𝑥 = 𝑧 → ((𝑥 ∈ On → (𝜑[suc 𝑥 / 𝑥]𝜑)) ↔ (𝑧 ∈ On → ([𝑧 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑))))
17 tfindes.2 . . 3 (𝑥 ∈ On → (𝜑[suc 𝑥 / 𝑥]𝜑))
1810, 16, 17chvar 2153 . 2 (𝑧 ∈ On → ([𝑧 / 𝑥]𝜑[suc 𝑧 / 𝑥]𝜑))
19 cbvralsv 3062 . . . 4 (∀𝑥𝑦 𝜑 ↔ ∀𝑧𝑦 [𝑧 / 𝑥]𝜑)
20 sbsbc 3310 . . . . 5 ([𝑧 / 𝑥]𝜑[𝑧 / 𝑥]𝜑)
2120ralbii 2867 . . . 4 (∀𝑧𝑦 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧𝑦 [𝑧 / 𝑥]𝜑)
2219, 21bitri 262 . . 3 (∀𝑥𝑦 𝜑 ↔ ∀𝑧𝑦 [𝑧 / 𝑥]𝜑)
23 tfindes.3 . . 3 (Lim 𝑦 → (∀𝑥𝑦 𝜑[𝑦 / 𝑥]𝜑))
2422, 23syl5bir 231 . 2 (Lim 𝑦 → (∀𝑧𝑦 [𝑧 / 𝑥]𝜑[𝑦 / 𝑥]𝜑))
251, 2, 3, 4, 5, 18, 24tfinds 6826 1 (𝑥 ∈ On → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  [wsb 1830  wcel 1938  wral 2800  [wsbc 3306  c0 3777  Oncon0 5530  Lim wlim 5531  suc csuc 5532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6722
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536
This theorem is referenced by:  tfinds2  6830
  Copyright terms: Public domain W3C validator