![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tfindes | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
tfindes.1 | ⊢ [∅ / 𝑥]𝜑 |
tfindes.2 | ⊢ (𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) |
tfindes.3 | ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 𝜑 → [𝑦 / 𝑥]𝜑)) |
Ref | Expression |
---|---|
tfindes | ⊢ (𝑥 ∈ On → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 3654 | . 2 ⊢ (𝑦 = ∅ → ([𝑦 / 𝑥]𝜑 ↔ [∅ / 𝑥]𝜑)) | |
2 | dfsbcq 3654 | . 2 ⊢ (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
3 | dfsbcq 3654 | . 2 ⊢ (𝑦 = suc 𝑧 → ([𝑦 / 𝑥]𝜑 ↔ [suc 𝑧 / 𝑥]𝜑)) | |
4 | sbceq2a 3664 | . 2 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | |
5 | tfindes.1 | . 2 ⊢ [∅ / 𝑥]𝜑 | |
6 | nfv 1957 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ On | |
7 | nfsbc1v 3672 | . . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑 | |
8 | nfsbc1v 3672 | . . . . 5 ⊢ Ⅎ𝑥[suc 𝑧 / 𝑥]𝜑 | |
9 | 7, 8 | nfim 1943 | . . . 4 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜑 → [suc 𝑧 / 𝑥]𝜑) |
10 | 6, 9 | nfim 1943 | . . 3 ⊢ Ⅎ𝑥(𝑧 ∈ On → ([𝑧 / 𝑥]𝜑 → [suc 𝑧 / 𝑥]𝜑)) |
11 | eleq1w 2842 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ On ↔ 𝑧 ∈ On)) | |
12 | sbceq1a 3663 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
13 | suceq 6043 | . . . . . 6 ⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) | |
14 | 13 | sbceq1d 3657 | . . . . 5 ⊢ (𝑥 = 𝑧 → ([suc 𝑥 / 𝑥]𝜑 ↔ [suc 𝑧 / 𝑥]𝜑)) |
15 | 12, 14 | imbi12d 336 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝜑 → [suc 𝑥 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝜑 → [suc 𝑧 / 𝑥]𝜑))) |
16 | 11, 15 | imbi12d 336 | . . 3 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) ↔ (𝑧 ∈ On → ([𝑧 / 𝑥]𝜑 → [suc 𝑧 / 𝑥]𝜑)))) |
17 | tfindes.2 | . . 3 ⊢ (𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑)) | |
18 | 10, 16, 17 | chvar 2360 | . 2 ⊢ (𝑧 ∈ On → ([𝑧 / 𝑥]𝜑 → [suc 𝑧 / 𝑥]𝜑)) |
19 | cbvralsv 3378 | . . . 4 ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ ∀𝑧 ∈ 𝑦 [𝑧 / 𝑥]𝜑) | |
20 | sbsbc 3656 | . . . . 5 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑) | |
21 | 20 | ralbii 3162 | . . . 4 ⊢ (∀𝑧 ∈ 𝑦 [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ 𝑦 [𝑧 / 𝑥]𝜑) |
22 | 19, 21 | bitri 267 | . . 3 ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ ∀𝑧 ∈ 𝑦 [𝑧 / 𝑥]𝜑) |
23 | tfindes.3 | . . 3 ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 𝜑 → [𝑦 / 𝑥]𝜑)) | |
24 | 22, 23 | syl5bir 235 | . 2 ⊢ (Lim 𝑦 → (∀𝑧 ∈ 𝑦 [𝑧 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜑)) |
25 | 1, 2, 3, 4, 5, 18, 24 | tfinds 7339 | 1 ⊢ (𝑥 ∈ On → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 [wsb 2011 ∈ wcel 2107 ∀wral 3090 [wsbc 3652 ∅c0 4141 Oncon0 5978 Lim wlim 5979 suc csuc 5980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-tr 4990 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-we 5318 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 |
This theorem is referenced by: tfinds2 7343 |
Copyright terms: Public domain | W3C validator |