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 rabeq2i ( 𝑥 ∈ On ↔ ( 𝑥 ∈ On ∧ 𝜑 ) )
33 32 simprbi ( 𝑥 ∈ On → 𝜑 )