This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
Assertion tfis ( 𝑥 ∈ On → 𝜑 )

Proof

Step Hyp Ref Expression
1 tfis.1 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
2 ssrab2 ⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
3 nfcv ⊢ Ⅎ 𝑥 𝑧
4 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝜑 }
5 3 4 nfss ⊢ Ⅎ 𝑥 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 }
6 4 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 }
7 5 6 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } )
8 dfss3 ⊢ ( 𝑥 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } )
9 sseq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ) )
10 8 9 bitr3id ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ) )
11 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑥 ∈ On ∧ 𝜑 ) )
12 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) )
13 11 12 bitr3id ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ On ∧ 𝜑 ) ↔ 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) )
14 10 13 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝑥 ∈ On ∧ 𝜑 ) ) ↔ ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) )
15 sbequ ⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
16 nfcv ⊢ Ⅎ 𝑥 On
17 nfcv ⊢ Ⅎ 𝑤 On
18 nfv ⊢ Ⅎ 𝑤 𝜑
19 nfs1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
20 sbequ12 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
21 16 17 18 19 20 cbvrabw ⊢ { 𝑥 ∈ On ∣ 𝜑 } = { 𝑤 ∈ On ∣ [ 𝑤 / 𝑥 ] 𝜑 }
22 15 21 elrab2 ⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑦 ∈ On ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
23 22 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → [ 𝑦 / 𝑥 ] 𝜑 )
24 23 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ∀ 𝑦 ∈ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )
25 24 1 syl5 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → 𝜑 ) )
26 25 anc2li ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝑥 ∈ On ∧ 𝜑 ) ) )
27 3 7 14 26 vtoclgaf ⊢ ( 𝑧 ∈ On → ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) )
28 27 rgen ⊢ ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } )
29 tfi ⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) → { 𝑥 ∈ On ∣ 𝜑 } = On )
30 2 28 29 mp2an ⊢ { 𝑥 ∈ On ∣ 𝜑 } = On
31 30 eqcomi ⊢ On = { 𝑥 ∈ On ∣ 𝜑 }
32 31 reqabi ⊢ ( 𝑥 ∈ On ↔ ( 𝑥 ∈ On ∧ 𝜑 ) )
33 32 simprbi ⊢ ( 𝑥 ∈ On → 𝜑 )