MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssfi Unicode version

Theorem ssfi 7760
Description: A subset of a finite set is finite. Corollary 6G of [Enderton] p. 138. (Contributed by NM, 24-Jun-1998.)
Assertion
Ref Expression
ssfi

Proof of Theorem ssfi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 7559 . . 3
2 bren 7545 . . . . 5
3 f1ofo 5828 . . . . . . . . . . 11
4 imassrn 5353 . . . . . . . . . . . 12
5 forn 5803 . . . . . . . . . . . 12
64, 5syl5sseq 3551 . . . . . . . . . . 11
73, 6syl 16 . . . . . . . . . 10
8 ssnnfi 7759 . . . . . . . . . . 11
9 isfi 7559 . . . . . . . . . . 11
108, 9sylib 196 . . . . . . . . . 10
117, 10sylan2 474 . . . . . . . . 9
1211adantrr 716 . . . . . . . 8
13 f1of1 5820 . . . . . . . . . . . . . 14
14 f1ores 5835 . . . . . . . . . . . . . 14
1513, 14sylan 471 . . . . . . . . . . . . 13
16 vex 3112 . . . . . . . . . . . . . . . . 17
1716resex 5322 . . . . . . . . . . . . . . . 16
18 f1oeq1 5812 . . . . . . . . . . . . . . . 16
1917, 18spcev 3201 . . . . . . . . . . . . . . 15
20 bren 7545 . . . . . . . . . . . . . . 15
2119, 20sylibr 212 . . . . . . . . . . . . . 14
22 entr 7587 . . . . . . . . . . . . . 14
2321, 22sylan 471 . . . . . . . . . . . . 13
2415, 23sylan 471 . . . . . . . . . . . 12
2524ex 434 . . . . . . . . . . 11
2625reximdv 2931 . . . . . . . . . 10
27 isfi 7559 . . . . . . . . . 10
2826, 27syl6ibr 227 . . . . . . . . 9
2928adantl 466 . . . . . . . 8
3012, 29mpd 15 . . . . . . 7
3130exp32 605 . . . . . 6
3231exlimdv 1724 . . . . 5
332, 32syl5bi 217 . . . 4
3433rexlimiv 2943 . . 3
351, 34sylbi 195 . 2
3635imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808  C_wss 3475   class class class wbr 4452  rancrn 5005  |`cres 5006  "cima 5007  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592   com 6700   cen 7533   cfn 7536
This theorem is referenced by:  domfi  7761  infi  7763  finresfin  7765  diffi  7771  findcard3  7783  unfir  7808  fnfi  7818  fofinf1o  7821  cnvfi  7824  f1fi  7827  imafi  7833  mapfi  7836  ixpfi  7837  ixpfi2  7838  mptfi  7839  cnvimamptfin  7841  fisuppfi  7857  suppssfifsupp  7864  fsuppunbi  7870  snopfsupp  7872  fsuppres  7874  ressuppfi  7875  fsuppmptif  7879  fsuppco2  7882  fsuppcor  7883  sniffsupp  7889  elfiun  7910  marypha1lem  7913  wemapso2OLD  7998  wemapso2lem  7999  cantnfp1lem1  8118  oemapvali  8124  cantnfp1lem1OLD  8144  cantnflem1dOLD  8151  cantnflem1OLD  8152  mapfienOLD  8159  ackbij2lem1  8620  ackbij1lem11  8631  fin23lem26  8726  fin23lem23  8727  fin23lem21  8740  fin11a  8784  isfin1-3  8787  axcclem  8858  pwfseqlem4  9061  ssnn0fi  12094  hashun3  12452  hashss  12474  hashssdif  12475  hashsslei  12484  hashbclem  12501  hashf1lem2  12505  seqcoll2  12513  pr2pwpr  12520  isercolllem2  13488  isercoll  13490  fsum2dlem  13585  fsumcom2  13589  fsumless  13610  fsumabs  13615  fsumrlim  13625  fsumo1  13626  cvgcmpce  13632  fsumiun  13635  qshash  13639  incexclem  13648  incexc  13649  incexc2  13650  fprod2dlem  13784  fprodcom2  13788  bitsfi  14087  bitsinv1  14092  bitsinvp1  14099  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  phicl2  14298  phibnd  14301  hashdvds  14305  phiprmpw  14306  phimullem  14309  eulerthlem2  14312  eulerth  14313  sumhash  14415  prmreclem2  14435  prmreclem3  14436  prmreclem4  14437  prmreclem5  14438  1arith  14445  4sqlem11  14473  vdwlem11  14509  hashbccl  14521  ramlb  14537  0ram  14538  ramub1lem1  14544  ramub1lem2  14545  isstruct2  14641  lagsubg2  16262  lagsubg  16263  orbsta2  16352  symgbasfi  16411  symgfisg  16493  symggen2  16496  odcl2  16587  oddvds2  16588  sylow1lem2  16619  sylow1lem3  16620  sylow1lem4  16621  sylow1lem5  16622  odcau  16624  pgpssslw  16634  sylow2alem2  16638  sylow2a  16639  sylow2blem1  16640  sylow2blem3  16642  slwhash  16644  fislw  16645  sylow2  16646  sylow3lem1  16647  sylow3lem3  16649  sylow3lem4  16650  sylow3lem6  16652  cyggenod  16887  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumval3  16911  gsumzadd  16935  gsumzaddOLD  16937  gsumzsplitOLD  16945  gsumzinvOLD  16970  gsumsubOLD  16975  gsumpt  16988  gsumptOLD  16989  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  gsum2d2lem  17001  dprdfadd  17060  dprdfidOLD  17064  dprdfinvOLD  17066  dprdfaddOLD  17067  dmdprdsplitlemOLD  17085  dpjidclOLD  17114  ablfacrplem  17116  ablfacrp2  17118  ablfac1c  17122  ablfac1eulem  17123  ablfac1eu  17124  pgpfac1lem5  17130  pgpfaclem2  17133  pgpfaclem3  17134  ablfaclem3  17138  lcomfsupOLD  17549  lcomfsupp  17550  psrbaglecl  18019  psrbagaddcl  18020  psrbagaddclOLD  18021  psrbagcon  18022  psrbasOLD  18031  psrlidmOLD  18057  psrridmOLD  18059  mvridlemOLD  18075  mplsubg  18098  mpllss  18099  mplsubrglemOLD  18101  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplbas2OLD  18135  psrbagsn  18160  psrbagev1OLD  18178  evlslem6OLD  18182  psr1baslem  18224  funsnfsupOLD  18256  dsmmfi  18769  dsmmacl  18772  dsmmsubg  18774  dsmmlss  18775  frlmsslsp  18829  frlmsslspOLD  18830  mamures  18892  submabas  19080  mdetdiaglem  19100  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  maducoeval2  19142  madugsum  19145  fctop  19505  restfpw  19680  fincmp  19893  cmpfi  19908  bwth  19910  finlocfin  20021  lfinpfin  20025  locfincmp  20027  1stckgenlem  20054  ptbasfi  20082  ptcnplem  20122  ptcmpfi  20314  cfinfil  20394  ufinffr  20430  fin1aufil  20433  tsmsresOLD  20645  tsmsres  20646  xrge0gsumle  21338  xrge0tsms  21339  fsumcn  21374  rrxcph  21824  rrxmval  21832  ovoliunlem1  21913  ovolicc2lem4  21931  ovolicc2lem5  21932  i1fima  22085  i1fd  22088  itg1cl  22092  itg1ge0  22093  i1f0  22094  i1f1  22097  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulc  22110  itg1mulc  22111  i1fres  22112  itg10a  22117  itg1ge0a  22118  itg1climres  22121  mbfi1fseqlem4  22125  itgfsum  22233  dvmptfsum  22376  plyexmo  22709  aannenlem2  22725  aalioulem2  22729  birthday  23284  jensenlem1  23316  jensenlem2  23317  jensen  23318  wilthlem2  23343  ppifi  23379  prmdvdsfi  23381  0sgm  23418  sgmf  23419  sgmnncl  23421  ppiprm  23425  chtprm  23427  chtdif  23432  efchtdvds  23433  ppidif  23437  ppiltx  23451  mumul  23455  sqff1o  23456  fsumdvdsdiag  23460  fsumdvdscom  23461  dvdsflsumcom  23464  musum  23467  musumsum  23468  muinv  23469  fsumdvdsmul  23471  ppiub  23479  vmasum  23491  logfac2  23492  perfectlem2  23505  dchrfi  23530  dchrabs  23535  dchrptlem1  23539  dchrptlem2  23540  dchrpt  23542  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  chebbnd1lem1  23654  chtppilimlem1  23658  rplogsumlem2  23670  rpvmasumlem  23672  dchrvmasumlem1  23680  dchrisum0ff  23692  rpvmasum2  23697  dchrisum0re  23698  dchrisum0  23705  rplogsum  23712  dirith2  23713  vmalogdivsum2  23723  logsqvma  23727  logsqvma2  23728  selberg  23733  selberg34r  23756  pntsval2  23761  pntrlog2bndlem1  23762  cusgrafi  24482  wwlknfi  24738  hashwwlkext  24746  clwwlknfi  24778  qerclwwlknfi  24829  vdgrfiun  24902  eupath2lem3  24979  konigsberg  24987  relfi  27459  unifi3  27528  ffsrn  27552  gsumle  27770  xrge0tsmsd  27775  hasheuni  28091  sibfof  28282  sitgclg  28284  oddpwdc  28293  eulerpartlems  28299  eulerpartlemb  28307  eulerpartlemmf  28314  eulerpartlemgf  28318  eulerpartlemgs2  28319  coinfliplem  28417  coinflippv  28422  ballotlemfelz  28429  ballotlemfp1  28430  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  ballotlemsup  28443  ballotlemfg  28464  ballotlemfrc  28465  ballotlemfrceq  28467  ballotth  28476  deranglem  28610  subfacp1lem3  28626  subfacp1lem5  28628  subfacp1lem6  28629  erdszelem2  28636  erdszelem8  28642  erdsze2lem2  28648  snmlff  28774  mvrsfpw  28866  itg2addnclem2  30067  finminlem  30136  nnubfi  30243  nninfnub  30244  sstotbnd2  30270  cntotbnd  30292  rencldnfilem  30754  jm2.22  30937  jm2.23  30938  filnm  31036  phisum  31159  fprodexp  31600  fprodabs2  31602  mccllem  31605  sumnnodd  31636  fprodcncf  31704  dvmptfprod  31742  dvnprodlem1  31743  dvnprodlem2  31744  fourierdlem25  31914  fourierdlem37  31926  fourierdlem51  31940  fourierdlem79  31968  fouriersw  32014  etransclem16  32033  etransclem24  32041  etransclem33  32050  etransclem44  32061  rmsuppfi  32966  mndpsuppfi  32968  scmsuppfi  32970  suppmptcfin  32972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-om 6701  df-er 7330  df-en 7537  df-fin 7540
  Copyright terms: Public domain W3C validator