Theorem tfis 4229

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.)

Hypothesis

Ref	Expression
tfis.1	⊢ (x ∈ On → (∀y ∈ x [y / x]φ → φ))

Assertion

Ref	Expression
tfis	⊢ (x ∈ On → φ)

Distinct variable groups:   φ,y   x,y

Allowed substitution hint:   φ(x)

Proof of Theorem tfis

Dummy variables w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 2998	. . . . 5 ⊢ {x ∈ On ∣ φ} ⊆ On
2		nfcv 2156	. . . . . . 7 ⊢ Ⅎxz
3		nfrab1 2463	. . . . . . . . 9 ⊢ Ⅎx{x ∈ On ∣ φ}
4	2, 3	nfss 2911	. . . . . . . 8 ⊢ Ⅎx z ⊆ {x ∈ On ∣ φ}
5	3	nfcri 2150	. . . . . . . 8 ⊢ Ⅎx z ∈ {x ∈ On ∣ φ}
6	4, 5	nfim 1442	. . . . . . 7 ⊢ Ⅎx(z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})
7		dfss3 2908	. . . . . . . . 9 ⊢ (x ⊆ {x ∈ On ∣ φ} ↔ ∀y ∈ x y ∈ {x ∈ On ∣ φ})
8		sseq1 2939	. . . . . . . . 9 ⊢ (x = z → (x ⊆ {x ∈ On ∣ φ} ↔ z ⊆ {x ∈ On ∣ φ}))
9	7, 8	syl5bbr 183	. . . . . . . 8 ⊢ (x = z → (∀y ∈ x y ∈ {x ∈ On ∣ φ} ↔ z ⊆ {x ∈ On ∣ φ}))
10		rabid 2459	. . . . . . . . 9 ⊢ (x ∈ {x ∈ On ∣ φ} ↔ (x ∈ On ∧ φ))
11		eleq1 2078	. . . . . . . . 9 ⊢ (x = z → (x ∈ {x ∈ On ∣ φ} ↔ z ∈ {x ∈ On ∣ φ}))
12	10, 11	syl5bbr 183	. . . . . . . 8 ⊢ (x = z → ((x ∈ On ∧ φ) ↔ z ∈ {x ∈ On ∣ φ}))
13	9, 12	imbi12d 223	. . . . . . 7 ⊢ (x = z → ((∀y ∈ x y ∈ {x ∈ On ∣ φ} → (x ∈ On ∧ φ)) ↔ (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})))
14		sbequ 1699	. . . . . . . . . . . 12 ⊢ (w = y → ([w / x]φ ↔ [y / x]φ))
15		nfcv 2156	. . . . . . . . . . . . 13 ⊢ ℲxOn
16		nfcv 2156	. . . . . . . . . . . . 13 ⊢ ℲwOn
17		nfv 1398	. . . . . . . . . . . . 13 ⊢ Ⅎwφ
18		nfs1v 1793	. . . . . . . . . . . . 13 ⊢ Ⅎx[w / x]φ
19		sbequ12 1632	. . . . . . . . . . . . 13 ⊢ (x = w → (φ ↔ [w / x]φ))
20	15, 16, 17, 18, 19	cbvrab 2529	. . . . . . . . . . . 12 ⊢ {x ∈ On ∣ φ} = {w ∈ On ∣ [w / x]φ}
21	14, 20	elrab2 2673	. . . . . . . . . . 11 ⊢ (y ∈ {x ∈ On ∣ φ} ↔ (y ∈ On ∧ [y / x]φ))
22	21	simprbi 260	. . . . . . . . . 10 ⊢ (y ∈ {x ∈ On ∣ φ} → [y / x]φ)
23	22	ralimi 2358	. . . . . . . . 9 ⊢ (∀y ∈ x y ∈ {x ∈ On ∣ φ} → ∀y ∈ x [y / x]φ)
24		tfis.1	. . . . . . . . 9 ⊢ (x ∈ On → (∀y ∈ x [y / x]φ → φ))
25	23, 24	syl5 28	. . . . . . . 8 ⊢ (x ∈ On → (∀y ∈ x y ∈ {x ∈ On ∣ φ} → φ))
26	25	anc2li 312	. . . . . . 7 ⊢ (x ∈ On → (∀y ∈ x y ∈ {x ∈ On ∣ φ} → (x ∈ On ∧ φ)))
27	2, 6, 13, 26	vtoclgaf 2591	. . . . . 6 ⊢ (z ∈ On → (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ}))
28	27	rgen 2348	. . . . 5 ⊢ ∀z ∈ On (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})
29		tfi 4228	. . . . 5 ⊢ (({x ∈ On ∣ φ} ⊆ On ∧ ∀z ∈ On (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})) → {x ∈ On ∣ φ} = On)
30	1, 28, 29	mp2an 404	. . . 4 ⊢ {x ∈ On ∣ φ} = On
31	30	eqcomi 2022	. . 3 ⊢ On = {x ∈ On ∣ φ}
32	31	rabeq2i 2528	. 2 ⊢ (x ∈ On ↔ (x ∈ On ∧ φ))
33	32	simprbi 260	1 ⊢ (x ∈ On → φ)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1226   ∈ wcel 1370  [wsb 1623  ∀wral 2280  {crab 2284   ⊆ wss 2890  Oncon0 4045

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-setind 4200

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-in 2897  df-ss 2904  df-uni 3551  df-tr 3825  df-iord 4048  df-on 4050

This theorem is referenced by:  tfis2f  4230