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 → 𝜑 )