Theorem tfis 4249

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 3019	. . . . 5 ⊢ {x ∈ On ∣ φ} ⊆ On
2		nfcv 2175	. . . . . . 7 ⊢ Ⅎxz
3		nfrab1 2483	. . . . . . . . 9 ⊢ Ⅎx{x ∈ On ∣ φ}
4	2, 3	nfss 2932	. . . . . . . 8 ⊢ Ⅎx z ⊆ {x ∈ On ∣ φ}
5	3	nfcri 2169	. . . . . . . 8 ⊢ Ⅎx z ∈ {x ∈ On ∣ φ}
6	4, 5	nfim 1461	. . . . . . 7 ⊢ Ⅎx(z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})
7		dfss3 2929	. . . . . . . . 9 ⊢ (x ⊆ {x ∈ On ∣ φ} ↔ ∀y ∈ x y ∈ {x ∈ On ∣ φ})
8		sseq1 2960	. . . . . . . . 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 2479	. . . . . . . . 9 ⊢ (x ∈ {x ∈ On ∣ φ} ↔ (x ∈ On ∧ φ))
11		eleq1 2097	. . . . . . . . 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 1718	. . . . . . . . . . . 12 ⊢ (w = y → ([w / x]φ ↔ [y / x]φ))
15		nfcv 2175	. . . . . . . . . . . . 13 ⊢ ℲxOn
16		nfcv 2175	. . . . . . . . . . . . 13 ⊢ ℲwOn
17		nfv 1418	. . . . . . . . . . . . 13 ⊢ Ⅎwφ
18		nfs1v 1812	. . . . . . . . . . . . 13 ⊢ Ⅎx[w / x]φ
19		sbequ12 1651	. . . . . . . . . . . . 13 ⊢ (x = w → (φ ↔ [w / x]φ))
20	15, 16, 17, 18, 19	cbvrab 2549	. . . . . . . . . . . 12 ⊢ {x ∈ On ∣ φ} = {w ∈ On ∣ [w / x]φ}
21	14, 20	elrab2 2694	. . . . . . . . . . 11 ⊢ (y ∈ {x ∈ On ∣ φ} ↔ (y ∈ On ∧ [y / x]φ))
22	21	simprbi 260	. . . . . . . . . 10 ⊢ (y ∈ {x ∈ On ∣ φ} → [y / x]φ)
23	22	ralimi 2378	. . . . . . . . 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 2612	. . . . . 6 ⊢ (z ∈ On → (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ}))
28	27	rgen 2368	. . . . 5 ⊢ ∀z ∈ On (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})
29		tfi 4248	. . . . 5 ⊢ (({x ∈ On ∣ φ} ⊆ On ∧ ∀z ∈ On (z ⊆ {x ∈ On ∣ φ} → z ∈ {x ∈ On ∣ φ})) → {x ∈ On ∣ φ} = On)
30	1, 28, 29	mp2an 402	. . . 4 ⊢ {x ∈ On ∣ φ} = On
31	30	eqcomi 2041	. . 3 ⊢ On = {x ∈ On ∣ φ}
32	31	rabeq2i 2548	. 2 ⊢ (x ∈ On ↔ (x ∈ On ∧ φ))
33	32	simprbi 260	1 ⊢ (x ∈ On → φ)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242   ∈ wcel 1390  [wsb 1642  ∀wral 2300  {crab 2304   ⊆ wss 2911  Oncon0 4066

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-in 2918  df-ss 2925  df-uni 3572  df-tr 3846  df-iord 4069  df-on 4071

This theorem is referenced by:  tfis2f  4250