Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfi Unicode version

Theorem tfi 4410
 Description: The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if is a class of ordinal numbers with the property that every ordinal number included in also belongs to , then every ordinal number is in . (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
tfi
Distinct variable group:   ,

Proof of Theorem tfi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-ral 2365 . . . . . . 7
2 imdi 249 . . . . . . . 8
32albii 1405 . . . . . . 7
41, 3bitri 183 . . . . . 6
5 dfss2 3015 . . . . . . . . . 10
65imbi2i 225 . . . . . . . . 9
7 19.21v 1802 . . . . . . . . 9
86, 7bitr4i 186 . . . . . . . 8
98imbi1i 237 . . . . . . 7
109albii 1405 . . . . . 6
114, 10bitri 183 . . . . 5
12 simpl 108 . . . . . . . . . . 11
13 tron 4218 . . . . . . . . . . . . . 14
14 dftr2 3944 . . . . . . . . . . . . . 14
1513, 14mpbi 144 . . . . . . . . . . . . 13
1615spi 1475 . . . . . . . . . . . 12
1716spi 1475 . . . . . . . . . . 11
1812, 17jca 301 . . . . . . . . . 10
1918imim1i 60 . . . . . . . . 9
20 impexp 260 . . . . . . . . 9
21 impexp 260 . . . . . . . . . 10
22 bi2.04 247 . . . . . . . . . 10
2321, 22bitri 183 . . . . . . . . 9
2419, 20, 233imtr3i 199 . . . . . . . 8
2524alimi 1390 . . . . . . 7
2625imim1i 60 . . . . . 6
2726alimi 1390 . . . . 5
2811, 27sylbi 120 . . . 4
2928adantl 272 . . 3
30 sbim 1876 . . . . . . . . . 10
31 clelsb3 2193 . . . . . . . . . . 11
32 clelsb3 2193 . . . . . . . . . . 11
3331, 32imbi12i 238 . . . . . . . . . 10
3430, 33bitri 183 . . . . . . . . 9
3534ralbii 2385 . . . . . . . 8
36 df-ral 2365 . . . . . . . 8
3735, 36bitri 183 . . . . . . 7
3837imbi1i 237 . . . . . 6
3938albii 1405 . . . . 5
40 ax-setind 4366 . . . . 5
4139, 40sylbir 134 . . . 4
42 dfss2 3015 . . . 4
4341, 42sylibr 133 . . 3
4429, 43syl 14 . 2
45 eqss 3041 . . 3
4645biimpri 132 . 2
4744, 46syldan 277 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103  wal 1288   wceq 1290   wcel 1439  wsb 1693  wral 2360   wss 3000   wtr 3942  con0 4199 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-setind 4366 This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2622  df-in 3006  df-ss 3013  df-uni 3660  df-tr 3943  df-iord 4202  df-on 4204 This theorem is referenced by:  tfis  4411
 Copyright terms: Public domain W3C validator