Theorem tfi 3748

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.

See theorem tfindes 3757 or tfinds 3753 for the version involving basis and induction hypotheses.

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

Step	Hyp	Ref	Expression
1		eldifn 2563	. . . . . . . . 9 |- (x e. (On \ A) -> -. x e. A)
2	1	adantl 422	. . . . . . . 8 |- (((x e. On -> (x C_ A -> x e. A)) /\ x e. (On \ A)) -> -. x e. A)
3		difin0ss 2763	. . . . . . . . . . . . 13 |- (((On \ A) i^i x) = (/) -> (x C_ On -> x C_ A))
4		onss 3680	. . . . . . . . . . . . 13 |- (x e. On -> x C_ On)
5	3, 4	syl5com 63	. . . . . . . . . . . 12 |- (x e. On -> (((On \ A) i^i x) = (/) -> x C_ A))
6	5	imim1d 33	. . . . . . . . . . 11 |- (x e. On -> ((x C_ A -> x e. A) -> (((On \ A) i^i x) = (/) -> x e. A)))
7	6	a2i 10	. . . . . . . . . 10 |- ((x e. On -> (x C_ A -> x e. A)) -> (x e. On -> (((On \ A) i^i x) = (/) -> x e. A)))
8		eldifi 2562	. . . . . . . . . 10 |- (x e. (On \ A) -> x e. On)
9	7, 8	syl5 20	. . . . . . . . 9 |- ((x e. On -> (x C_ A -> x e. A)) -> (x e. (On \ A) -> (((On \ A) i^i x) = (/) -> x e. A)))
10	9	imp 375	. . . . . . . 8 |- (((x e. On -> (x C_ A -> x e. A)) /\ x e. (On \ A)) -> (((On \ A) i^i x) = (/) -> x e. A))
11	2, 10	mtod 122	. . . . . . 7 |- (((x e. On -> (x C_ A -> x e. A)) /\ x e. (On \ A)) -> -. ((On \ A) i^i x) = (/))
12	11	ex 400	. . . . . 6 |- ((x e. On -> (x C_ A -> x e. A)) -> (x e. (On \ A) -> -. ((On \ A) i^i x) = (/)))
13	12	ralimi2 1999	. . . . 5 |- (A.x e. On (x C_ A -> x e. A) -> A.x e. (On \ A) -. ((On \ A) i^i x) = (/))
14		ralnex 1947	. . . . 5 |- (A.x e. (On \ A) -. ((On \ A) i^i x) = (/) <-> -. E.x e. (On \ A)((On \ A) i^i x) = (/))
15	13, 14	sylib 214	. . . 4 |- (A.x e. On (x C_ A -> x e. A) -> -. E.x e. (On \ A)((On \ A) i^i x) = (/))
16		ssdif0 2758	. . . . . 6 |- (On C_ A <-> (On \ A) = (/))
17	16	necon3bbii 1866	. . . . 5 |- (-. On C_ A <-> (On \ A) =/= (/))
18		ordon 3674	. . . . . 6 |- Ord On
19		difss 2567	. . . . . 6 |- (On \ A) C_ On
20		tz7.5 3494	. . . . . 6 |- ((Ord On /\ (On \ A) C_ On /\ (On \ A) =/= (/)) -> E.x e. (On \ A)((On \ A) i^i x) = (/))
21	18, 19, 20	mp3an12 1028	. . . . 5 |- ((On \ A) =/= (/) -> E.x e. (On \ A)((On \ A) i^i x) = (/))
22	17, 21	sylbi 215	. . . 4 |- (-. On C_ A -> E.x e. (On \ A)((On \ A) i^i x) = (/))
23	15, 22	nsyl2 132	. . 3 |- (A.x e. On (x C_ A -> x e. A) -> On C_ A)
24	23	anim2i 360	. 2 |- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> (A C_ On /\ On C_ A))
25		eqss 2464	. 2 |- (A = On <-> (A C_ On /\ On C_ A))
26	24, 25	sylibr 216	1 |- ((A C_ On /\ A.x e. On (x C_ A -> x e. A)) -> A = On)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 239   = wceq 1136   e. wcel 1138   =/= wne 1854  A.wral 1939  E.wrex 1940   \ cdif 2423   i^i cin 2425   C_ wss 2426  (/)c0 2701  Ord word 3471  Oncon0 3472

This theorem is referenced by:  tfis 3749  tfisg 13704

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476

Copyright terms: Public domain