Metamath Proof Explorer

Theorem tfis

Description: Transfinite Induction Schema. If all ordinal numbers less than a given number x 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)

Ref Expression
Hypothesis tfis.1 ⊢x∈On→∀y∈xyxφ→φ
Assertion tfis ⊢x∈On→φ

Proof

Step Hyp Ref Expression
1 tfis.1 ⊢x∈On→∀y∈xyxφ→φ
2 ssrab2 ⊢x∈On|φ⊆On
3 nfcv ⊢Ⅎ_xz
4 nfrab1 ⊢Ⅎ_xx∈On|φ
5 3 4 nfss ⊢Ⅎxz⊆x∈On|φ
6 4 nfcri ⊢Ⅎxz∈x∈On|φ
7 5 6 nfim ⊢Ⅎxz⊆x∈On|φ→z∈x∈On|φ
8 dfss3 ⊢x⊆x∈On|φ↔∀y∈xy∈x∈On|φ
9 sseq1 ⊢x=z→x⊆x∈On|φ↔z⊆x∈On|φ
10 8 9 bitr3id ⊢x=z→∀y∈xy∈x∈On|φ↔z⊆x∈On|φ
11 rabid ⊢x∈x∈On|φ↔x∈On∧φ
12 eleq1w ⊢x=z→x∈x∈On|φ↔z∈x∈On|φ
13 11 12 bitr3id ⊢x=z→x∈On∧φ↔z∈x∈On|φ
14 10 13 imbi12d ⊢x=z→∀y∈xy∈x∈On|φ→x∈On∧φ↔z⊆x∈On|φ→z∈x∈On|φ
15 sbequ ⊢w=y→wxφ↔yxφ
16 nfcv ⊢Ⅎ_xOn
17 nfcv ⊢Ⅎ_wOn
18 nfv ⊢Ⅎwφ
19 nfs1v ⊢Ⅎxwxφ
20 sbequ12 ⊢x=w→φ↔wxφ
21 16 17 18 19 20 cbvrabw ⊢x∈On|φ=w∈On|wxφ
22 15 21 elrab2 ⊢y∈x∈On|φ↔y∈On∧yxφ
23 22 simprbi ⊢y∈x∈On|φ→yxφ
24 23 ralimi ⊢∀y∈xy∈x∈On|φ→∀y∈xyxφ
25 24 1 syl5 ⊢x∈On→∀y∈xy∈x∈On|φ→φ
26 25 anc2li ⊢x∈On→∀y∈xy∈x∈On|φ→x∈On∧φ
27 3 7 14 26 vtoclgaf ⊢z∈On→z⊆x∈On|φ→z∈x∈On|φ
28 27 rgen ⊢∀z∈Onz⊆x∈On|φ→z∈x∈On|φ
29 tfi ⊢x∈On|φ⊆On∧∀z∈Onz⊆x∈On|φ→z∈x∈On|φ→x∈On|φ=On
30 2 28 29 mp2an ⊢x∈On|φ=On
31 30 eqcomi ⊢On=x∈On|φ
32 31 reqabi ⊢x∈On↔x∈On∧φ
33 32 simprbi ⊢x∈On→φ