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 ∈ x y x φ → φ
Assertion tfis ⊢ x ∈ On → φ

Proof

Step Hyp Ref Expression
1 tfis.1 ⊢ x ∈ On → ∀ y ∈ x y x φ → φ
2 ssrab2 ⊢ x ∈ On | φ ⊆ On
3 nfcv ⊢ Ⅎ _ x z
4 nfrab1 ⊢ Ⅎ _ x x ∈ On | φ
5 3 4 nfss ⊢ Ⅎ x z ⊆ x ∈ On | φ
6 4 nfcri ⊢ Ⅎ x z ∈ x ∈ On | φ
7 5 6 nfim ⊢ Ⅎ x z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
8 dfss3 ⊢ x ⊆ x ∈ On | φ ↔ ∀ y ∈ x y ∈ x ∈ On | φ
9 sseq1 ⊢ x = z → x ⊆ x ∈ On | φ ↔ z ⊆ x ∈ On | φ
10 8 9 bitr3id ⊢ x = z → ∀ y ∈ x y ∈ 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 ∈ x y ∈ x ∈ On | φ → x ∈ On ∧ φ ↔ z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
15 sbequ ⊢ w = y → w x φ ↔ y x φ
16 nfcv ⊢ Ⅎ _ x On
17 nfcv ⊢ Ⅎ _ w On
18 nfv ⊢ Ⅎ w φ
19 nfs1v ⊢ Ⅎ x w x φ
20 sbequ12 ⊢ x = w → φ ↔ w x φ
21 16 17 18 19 20 cbvrabw ⊢ x ∈ On | φ = w ∈ On | w x φ
22 15 21 elrab2 ⊢ y ∈ x ∈ On | φ ↔ y ∈ On ∧ y x φ
23 22 simprbi ⊢ y ∈ x ∈ On | φ → y x φ
24 23 ralimi ⊢ ∀ y ∈ x y ∈ x ∈ On | φ → ∀ y ∈ x y x φ
25 24 1 syl5 ⊢ x ∈ On → ∀ y ∈ x y ∈ x ∈ On | φ → φ
26 25 anc2li ⊢ x ∈ On → ∀ y ∈ x y ∈ x ∈ On | φ → x ∈ On ∧ φ
27 3 7 14 26 vtoclgaf ⊢ z ∈ On → z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
28 27 rgen ⊢ ∀ z ∈ On z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
29 tfi ⊢ x ∈ On | φ ⊆ On ∧ ∀ z ∈ On z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ → x ∈ On | φ = On
30 2 28 29 mp2an ⊢ x ∈ On | φ = On
31 30 eqcomi ⊢ On = x ∈ On | φ
32 31 rabeq2i ⊢ x ∈ On ↔ x ∈ On ∧ φ
33 32 simprbi ⊢ x ∈ On → φ