NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  spfininduct Unicode version

Theorem spfininduct 4540
Description: Inductive principle for Spfin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Assertion
Ref Expression
spfininduct Ncfin Spfin Sfin Spfin
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem spfininduct
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 spfinex 4537 . . 3 Spfin
2 inexg 4100 . . 3 Spfin Spfin
31, 2mpan 651 . 2 Spfin
4 ncvspfin 4538 . . 3 Ncfin Spfin
5 elin 3219 . . . 4 Ncfin Spfin Ncfin Spfin Ncfin
65biimpri 197 . . 3 Ncfin Spfin Ncfin Ncfin Spfin
74, 6mpan 651 . 2 Ncfin Ncfin Spfin
8 elin 3219 . . . . 5 Spfin Spfin
9 spfinsfincl 4539 . . . . . . . . . . . . . 14 Spfin Sfin Spfin
109adantrl 696 . . . . . . . . . . . . 13 Spfin Sfin Spfin
1110a1d 22 . . . . . . . . . . . 12 Spfin Sfin Spfin
1211ancrd 537 . . . . . . . . . . 11 Spfin Sfin Spfin
13 elin 3219 . . . . . . . . . . 11 Spfin Spfin
1412, 13syl6ibr 218 . . . . . . . . . 10 Spfin Sfin Spfin
1514ex 423 . . . . . . . . 9 Spfin Sfin Spfin
1615a2d 23 . . . . . . . 8 Spfin Sfin Sfin Spfin
1716exp4a 589 . . . . . . 7 Spfin Sfin Sfin Spfin
1817a2i 12 . . . . . 6 Spfin Sfin Spfin Sfin Spfin
1918imp3a 420 . . . . 5 Spfin Sfin Spfin Sfin Spfin
208, 19syl5bi 208 . . . 4 Spfin Sfin Spfin Sfin Spfin
21202alimi 1560 . . 3 Spfin Sfin Spfin Sfin Spfin
22 df-ral 2619 . . . 4 Spfin Sfin Spfin Sfin
23 19.21v 1890 . . . . 5 Spfin Sfin Spfin Sfin
2423albii 1566 . . . 4 Spfin Sfin Spfin Sfin
2522, 24bitr4i 243 . . 3 Spfin Sfin Spfin Sfin
26 df-ral 2619 . . . 4 Spfin Sfin Spfin Spfin Sfin Spfin
27 19.21v 1890 . . . . 5 Spfin Sfin Spfin Spfin Sfin Spfin
2827albii 1566 . . . 4 Spfin Sfin Spfin Spfin Sfin Spfin
2926, 28bitr4i 243 . . 3 Spfin Sfin Spfin Spfin Sfin Spfin
3021, 25, 293imtr4i 257 . 2 Spfin Sfin Spfin Sfin Spfin
31 df-spfin 4447 . . . 4 Spfin Ncfin Sfin
32 eleq2 2414 . . . . . . . . 9 Spfin Ncfin Ncfin Spfin
33 eleq2 2414 . . . . . . . . . . . 12 Spfin Spfin
3433imbi2d 307 . . . . . . . . . . 11 Spfin Sfin Sfin Spfin
3534albidv 1625 . . . . . . . . . 10 Spfin Sfin Sfin Spfin
3635raleqbi1dv 2815 . . . . . . . . 9 Spfin Sfin Spfin Sfin Spfin
3732, 36anbi12d 691 . . . . . . . 8 Spfin Ncfin Sfin Ncfin Spfin Spfin Sfin Spfin
3837elabg 2986 . . . . . . 7 Spfin Spfin Ncfin Sfin Ncfin Spfin Spfin Sfin Spfin
3938biimprd 214 . . . . . 6 Spfin Ncfin Spfin Spfin Sfin Spfin Spfin Ncfin Sfin
40393impib 1149 . . . . 5 Spfin Ncfin Spfin Spfin Sfin Spfin Spfin Ncfin Sfin
41 intss1 3941 . . . . 5 Spfin Ncfin Sfin Ncfin Sfin Spfin
4240, 41syl 15 . . . 4 Spfin Ncfin Spfin Spfin Sfin Spfin Ncfin Sfin Spfin
4331, 42syl5eqss 3315 . . 3 Spfin Ncfin Spfin Spfin Sfin Spfin Spfin Spfin
44 inss2 3476 . . 3 Spfin
4543, 44syl6ss 3284 . 2 Spfin Ncfin Spfin Spfin Sfin Spfin Spfin
463, 7, 30, 45syl3an 1224 1 Ncfin Spfin Sfin Spfin
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358   w3a 934  wal 1540   wceq 1642   wcel 1710  cab 2339  wral 2614  cvv 2859   cin 3208   wss 3257  cint 3926   Ncfin cncfin 4434   Sfin wsfin 4438   Spfin cspfin 4439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-iota 4339  df-addc 4378  df-nnc 4379  df-ncfin 4442  df-sfin 4446  df-spfin 4447
This theorem is referenced by:  vfinspnn  4541  vfinspss  4551  vfinspclt  4552
  Copyright terms: Public domain W3C validator