Theorem tfi 4248

Description: The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A, then every ordinal number is in A.

(Contributed by NM, 18-Feb-2004.)

Assertion

Ref	Expression
tfi	|- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> A = On)

Distinct variable group:   x,A

Proof of Theorem tfi

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ral 2305	. . . . . . 7 |- (A.x e. On (x C_ A -> x e. A) <-> A.x(x e. On -> (x C_ A -> x e. A)))
2		imdi 239	. . . . . . . 8 |- ((x e. On -> (x C_ A -> x e. A)) <-> ((x e. On -> x C_ A) -> (x e. On -> x e. A)))
3	2	albii 1356	. . . . . . 7 |- (A.x(x e. On -> (x C_ A -> x e. A)) <-> A.x((x e. On -> x C_ A) -> (x e. On -> x e. A)))
4	1, 3	bitri 173	. . . . . 6 |- (A.x e. On (x C_ A -> x e. A) <-> A.x((x e. On -> x C_ A) -> (x e. On -> x e. A)))
5		dfss2 2928	. . . . . . . . . 10 |- (x C_ A <-> A.y(y e. x -> y e. A))
6	5	imbi2i 215	. . . . . . . . 9 |- ((x e. On -> x C_ A) <-> (x e. On -> A.y(y e. x -> y e. A)))
7		19.21v 1750	. . . . . . . . 9 |- (A.y(x e. On -> (y e. x -> y e. A)) <-> (x e. On -> A.y(y e. x -> y e. A)))
8	6, 7	bitr4i 176	. . . . . . . 8 |- ((x e. On -> x C_ A) <-> A.y(x e. On -> (y e. x -> y e. A)))
9	8	imbi1i 227	. . . . . . 7 |- (((x e. On -> x C_ A) -> (x e. On -> x e. A)) <-> (A.y(x e. On -> (y e. x -> y e. A)) -> (x e. On -> x e. A)))
10	9	albii 1356	. . . . . 6 |- (A.x((x e. On -> x C_ A) -> (x e. On -> x e. A)) <-> A.x(A.y(x e. On -> (y e. x -> y e. A)) -> (x e. On -> x e. A)))
11	4, 10	bitri 173	. . . . 5 |- (A.x e. On (x C_ A -> x e. A) <-> A.x(A.y(x e. On -> (y e. x -> y e. A)) -> (x e. On -> x e. A)))
12		simpl 102	. . . . . . . . . . 11 |- ((y e. x /\ x e. On) -> y e. x)
13		tron 4085	. . . . . . . . . . . . . 14 |- Tr On
14		dftr2 3847	. . . . . . . . . . . . . 14 |- ( Tr On <-> A.yA.x((y e. x /\ x e. On) -> y e. On))
15	13, 14	mpbi 133	. . . . . . . . . . . . 13 |- A.yA.x((y e. x /\ x e. On) -> y e. On)
16	15	spi 1426	. . . . . . . . . . . 12 |- A.x((y e. x /\ x e. On) -> y e. On)
17	16	spi 1426	. . . . . . . . . . 11 |- ((y e. x /\ x e. On) -> y e. On)
18	12, 17	jca 290	. . . . . . . . . 10 |- ((y e. x /\ x e. On) -> (y e. x /\ y e. On))
19	18	imim1i 54	. . . . . . . . 9 |- (((y e. x /\ y e. On) -> y e. A) -> ((y e. x /\ x e. On) -> y e. A))
20		impexp 250	. . . . . . . . 9 |- (((y e. x /\ y e. On) -> y e. A) <-> (y e. x -> (y e. On -> y e. A)))
21		impexp 250	. . . . . . . . . 10 |- (((y e. x /\ x e. On) -> y e. A) <-> (y e. x -> (x e. On -> y e. A)))
22		bi2.04 237	. . . . . . . . . 10 |- ((y e. x -> (x e. On -> y e. A)) <-> (x e. On -> (y e. x -> y e. A)))
23	21, 22	bitri 173	. . . . . . . . 9 |- (((y e. x /\ x e. On) -> y e. A) <-> (x e. On -> (y e. x -> y e. A)))
24	19, 20, 23	3imtr3i 189	. . . . . . . 8 |- ((y e. x -> (y e. On -> y e. A)) -> (x e. On -> (y e. x -> y e. A)))
25	24	alimi 1341	. . . . . . 7 |- (A.y(y e. x -> (y e. On -> y e. A)) -> A.y(x e. On -> (y e. x -> y e. A)))
26	25	imim1i 54	. . . . . 6 |- ((A.y(x e. On -> (y e. x -> y e. A)) -> (x e. On -> x e. A)) -> (A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
27	26	alimi 1341	. . . . 5 |- (A.x(A.y(x e. On -> (y e. x -> y e. A)) -> (x e. On -> x e. A)) -> A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
28	11, 27	sylbi 114	. . . 4 |- (A.x e. On (x C_ A -> x e. A) -> A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
29	28	adantl 262	. . 3 |- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
30		sbim 1824	. . . . . . . . . 10 |- ([y / x](x e. On -> x e. A) <-> ([y / x]x e. On -> [y / x]x e. A))
31		clelsb3 2139	. . . . . . . . . . 11 |- ([y / x]x e. On <-> y e. On)
32		clelsb3 2139	. . . . . . . . . . 11 |- ([y / x]x e. A <-> y e. A)
33	31, 32	imbi12i 228	. . . . . . . . . 10 |- (([y / x]x e. On -> [y / x]x e. A) <-> (y e. On -> y e. A))
34	30, 33	bitri 173	. . . . . . . . 9 |- ([y / x](x e. On -> x e. A) <-> (y e. On -> y e. A))
35	34	ralbii 2324	. . . . . . . 8 |- (A.y e. x [y / x](x e. On -> x e. A) <-> A.y e. x (y e. On -> y e. A))
36		df-ral 2305	. . . . . . . 8 |- (A.y e. x (y e. On -> y e. A) <-> A.y(y e. x -> (y e. On -> y e. A)))
37	35, 36	bitri 173	. . . . . . 7 |- (A.y e. x [y / x](x e. On -> x e. A) <-> A.y(y e. x -> (y e. On -> y e. A)))
38	37	imbi1i 227	. . . . . 6 |- ((A.y e. x [y / x](x e. On -> x e. A) -> (x e. On -> x e. A)) <-> (A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
39	38	albii 1356	. . . . 5 |- (A.x(A.y e. x [y / x](x e. On -> x e. A) -> (x e. On -> x e. A)) <-> A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)))
40		ax-setind 4220	. . . . 5 |- (A.x(A.y e. x [y / x](x e. On -> x e. A) -> (x e. On -> x e. A)) -> A.x(x e. On -> x e. A))
41	39, 40	sylbir 125	. . . 4 |- (A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)) -> A.x(x e. On -> x e. A))
42		dfss2 2928	. . . 4 |- ( On C_ A <-> A.x(x e. On -> x e. A))
43	41, 42	sylibr 137	. . 3 |- (A.x(A.y(y e. x -> (y e. On -> y e. A)) -> (x e. On -> x e. A)) -> On C_ A)
44	29, 43	syl 14	. 2 |- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> On C_ A)
45		eqss 2954	. . 3 |- (A = On <-> (A C_ On /\ On C_ A))
46	45	biimpri 124	. 2 |- ((A C_ On /\ On C_ A) -> A = On)
47	44, 46	syldan 266	1 |- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> A = On)

Syntax hints:   -> wi 4   /\ wa 97  A.wal 1240   = wceq 1242   e. wcel 1390  [wsb 1642  A.wral 2300   C_ wss 2911   Tr wtr 3845   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-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:  tfis  4249