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

Theorem tfis 7051
Description: Transfinite Induction Schema. If all ordinal numbers less than a given number 𝑥 have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 20-Nov-2016.)
Hypothesis
Ref Expression
tfis.1 (𝑥 ∈ On → (∀𝑦𝑥 [𝑦 / 𝑥]𝜑𝜑))
Assertion
Ref Expression
tfis (𝑥 ∈ On → 𝜑)
Distinct variable groups:   𝜑,𝑦   𝑥,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem tfis
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3685 . . . . 5 {𝑥 ∈ On ∣ 𝜑} ⊆ On
2 nfcv 2763 . . . . . . 7 𝑥𝑧
3 nfrab1 3120 . . . . . . . . 9 𝑥{𝑥 ∈ On ∣ 𝜑}
42, 3nfss 3594 . . . . . . . 8 𝑥 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑}
53nfcri 2757 . . . . . . . 8 𝑥 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}
64, 5nfim 1824 . . . . . . 7 𝑥(𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})
7 dfss3 3590 . . . . . . . . 9 (𝑥 ⊆ {𝑥 ∈ On ∣ 𝜑} ↔ ∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑})
8 sseq1 3624 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 ⊆ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑}))
97, 8syl5bbr 274 . . . . . . . 8 (𝑥 = 𝑧 → (∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑}))
10 rabid 3114 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑥 ∈ On ∧ 𝜑))
11 eleq1 2688 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}))
1210, 11syl5bbr 274 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 ∈ On ∧ 𝜑) ↔ 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}))
139, 12imbi12d 334 . . . . . . 7 (𝑥 = 𝑧 → ((∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → (𝑥 ∈ On ∧ 𝜑)) ↔ (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})))
14 sbequ 2375 . . . . . . . . . . . 12 (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
15 nfcv 2763 . . . . . . . . . . . . 13 𝑥On
16 nfcv 2763 . . . . . . . . . . . . 13 𝑤On
17 nfv 1842 . . . . . . . . . . . . 13 𝑤𝜑
18 nfs1v 2436 . . . . . . . . . . . . 13 𝑥[𝑤 / 𝑥]𝜑
19 sbequ12 2110 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
2015, 16, 17, 18, 19cbvrab 3196 . . . . . . . . . . . 12 {𝑥 ∈ On ∣ 𝜑} = {𝑤 ∈ On ∣ [𝑤 / 𝑥]𝜑}
2114, 20elrab2 3364 . . . . . . . . . . 11 (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} ↔ (𝑦 ∈ On ∧ [𝑦 / 𝑥]𝜑))
2221simprbi 480 . . . . . . . . . 10 (𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → [𝑦 / 𝑥]𝜑)
2322ralimi 2951 . . . . . . . . 9 (∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → ∀𝑦𝑥 [𝑦 / 𝑥]𝜑)
24 tfis.1 . . . . . . . . 9 (𝑥 ∈ On → (∀𝑦𝑥 [𝑦 / 𝑥]𝜑𝜑))
2523, 24syl5 34 . . . . . . . 8 (𝑥 ∈ On → (∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → 𝜑))
2625anc2li 580 . . . . . . 7 (𝑥 ∈ On → (∀𝑦𝑥 𝑦 ∈ {𝑥 ∈ On ∣ 𝜑} → (𝑥 ∈ On ∧ 𝜑)))
272, 6, 13, 26vtoclgaf 3269 . . . . . 6 (𝑧 ∈ On → (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑}))
2827rgen 2921 . . . . 5 𝑧 ∈ On (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})
29 tfi 7050 . . . . 5 (({𝑥 ∈ On ∣ 𝜑} ⊆ On ∧ ∀𝑧 ∈ On (𝑧 ⊆ {𝑥 ∈ On ∣ 𝜑} → 𝑧 ∈ {𝑥 ∈ On ∣ 𝜑})) → {𝑥 ∈ On ∣ 𝜑} = On)
301, 28, 29mp2an 708 . . . 4 {𝑥 ∈ On ∣ 𝜑} = On
3130eqcomi 2630 . . 3 On = {𝑥 ∈ On ∣ 𝜑}
3231rabeq2i 3195 . 2 (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝜑))
3332simprbi 480 1 (𝑥 ∈ On → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1482  [wsb 1879  wcel 1989  wral 2911  {crab 2915  wss 3572  Oncon0 5721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-tr 4751  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-ord 5724  df-on 5725
This theorem is referenced by:  tfis2f  7052
  Copyright terms: Public domain W3C validator