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

Theorem ssfi 7798
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  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )

Proof of Theorem ssfi
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 7600 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7586 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5838 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5199 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5813 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3518 . . . . . . . . . . 11  |-  ( z : A -onto-> x  -> 
( z " B
)  C_  x )
73, 6syl 17 . . . . . . . . . 10  |-  ( z : A -1-1-onto-> x  ->  ( z
" B )  C_  x )
8 ssnnfi 7797 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7600 . . . . . . . . . . 11  |-  ( ( z " B )  e.  Fin  <->  E. y  e.  om  ( z " B )  ~~  y
)
108, 9sylib 199 . . . . . . . . . 10  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  E. y  e.  om  ( z " B
)  ~~  y )
117, 10sylan2 476 . . . . . . . . 9  |-  ( ( x  e.  om  /\  z : A -1-1-onto-> x )  ->  E. y  e.  om  ( z " B )  ~~  y
)
1211adantrr 721 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5830 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5845 . . . . . . . . . . . . . 14  |-  ( ( z : A -1-1-> x  /\  B  C_  A )  ->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) )
1513, 14sylan 473 . . . . . . . . . . . . 13  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( z  |`  B ) : B -1-1-onto-> ( z " B
) )
16 vex 3090 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5168 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5822 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 3179 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7586 . . . . . . . . . . . . . . 15  |-  ( B 
~~  ( z " B )  <->  E. x  x : B -1-1-onto-> ( z " B
) )
2119, 20sylibr 215 . . . . . . . . . . . . . 14  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  B  ~~  ( z " B
) )
22 entr 7628 . . . . . . . . . . . . . 14  |-  ( ( B  ~~  ( z
" B )  /\  ( z " B
)  ~~  y )  ->  B  ~~  y )
2321, 22sylan 473 . . . . . . . . . . . . 13  |-  ( ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2415, 23sylan 473 . . . . . . . . . . . 12  |-  ( ( ( z : A -1-1-onto-> x  /\  B  C_  A )  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2524ex 435 . . . . . . . . . . 11  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( ( z " B )  ~~  y  ->  B  ~~  y ) )
2625reximdv 2906 . . . . . . . . . 10  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  E. y  e.  om  B  ~~  y ) )
27 isfi 7600 . . . . . . . . . 10  |-  ( B  e.  Fin  <->  E. y  e.  om  B  ~~  y
)
2826, 27syl6ibr 230 . . . . . . . . 9  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  B  e.  Fin )
)
2928adantl 467 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  ( E. y  e.  om  (
z " B ) 
~~  y  ->  B  e.  Fin ) )
3012, 29mpd 15 . . . . . . 7  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  B  e.  Fin )
3130exp32 608 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1771 . . . . 5  |-  ( x  e.  om  ->  ( E. z  z : A
-1-1-onto-> x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
332, 32syl5bi 220 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
3433rexlimiv 2918 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C_  A  ->  B  e.  Fin ) )
351, 34sylbi 198 . 2  |-  ( A  e.  Fin  ->  ( B  C_  A  ->  B  e.  Fin ) )
3635imp 430 1  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1659    e. wcel 1870   E.wrex 2783    C_ wss 3442   class class class wbr 4426   ran crn 4855    |` cres 4856   "cima 4857   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600   omcom 6706    ~~ cen 7574   Fincfn 7577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-om 6707  df-er 7371  df-en 7578  df-fin 7581
This theorem is referenced by:  domfi  7799  infi  7801  finresfin  7803  diffi  7809  findcard3  7820  unfir  7845  fnfi  7855  fofinf1o  7858  cnvfi  7862  f1fi  7867  imafi  7873  mapfi  7876  ixpfi  7877  ixpfi2  7878  mptfi  7879  cnvimamptfin  7881  fisuppfi  7897  suppssfifsupp  7904  fsuppunbi  7910  snopfsupp  7912  fsuppres  7914  ressuppfi  7915  fsuppmptif  7919  fsuppco2  7922  fsuppcor  7923  sniffsupp  7929  elfiun  7950  marypha1lem  7953  wemapso2lem  8067  cantnfp1lem1  8182  oemapvali  8188  ackbij2lem1  8647  ackbij1lem11  8658  fin23lem26  8753  fin23lem23  8754  fin23lem21  8767  fin11a  8811  isfin1-3  8814  axcclem  8885  pwfseqlem4  9086  ssnn0fi  12194  hashun3  12560  hashss  12583  hashssdif  12584  hashsslei  12593  hashbclem  12610  hashf1lem2  12614  seqcoll2  12622  pr2pwpr  12629  isercolllem2  13707  isercoll  13709  fsum2dlem  13809  fsumcom2  13813  fsumless  13834  fsumabs  13839  fsumrlim  13849  fsumo1  13850  cvgcmpce  13856  fsumiun  13859  qshash  13863  incexclem  13872  incexc  13873  incexc2  13874  fprod2dlem  14012  fprodcom2  14016  bitsfi  14385  bitsinv1  14390  bitsinvp1  14397  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  sadasslem  14418  sadeq  14420  phicl2  14676  phibnd  14679  hashdvds  14683  phiprmpw  14684  phimullem  14687  eulerthlem2  14690  eulerth  14691  sumhash  14795  prmreclem2  14815  prmreclem3  14816  prmreclem4  14817  prmreclem5  14818  1arith  14825  4sqlem11  14853  vdwlem11  14895  hashbccl  14909  ramlb  14931  0ram  14932  ramub1lem1  14938  ramub1lem2  14939  prmgaplem3  14977  prmgaplem4  14978  isstruct2  15084  lagsubg2  16820  lagsubg  16821  orbsta2  16910  symgbasfi  16969  symgfisg  17051  symggen2  17054  odcl2  17145  oddvds2  17146  sylow1lem2  17177  sylow1lem3  17178  sylow1lem4  17179  sylow1lem5  17180  odcau  17182  pgpssslw  17192  sylow2alem2  17196  sylow2a  17197  sylow2blem1  17198  sylow2blem3  17200  slwhash  17202  fislw  17203  sylow2  17204  sylow3lem1  17205  sylow3lem3  17207  sylow3lem4  17208  sylow3lem6  17210  cyggenod  17445  gsumval3lem1  17465  gsumval3lem2  17466  gsumval3  17467  gsumzadd  17481  gsumpt  17520  gsum2dlem1  17528  gsum2dlem2  17529  gsum2d  17530  gsum2d2lem  17531  dprdfadd  17579  ablfacrplem  17624  ablfacrp2  17626  ablfac1c  17630  ablfac1eulem  17631  ablfac1eu  17632  pgpfac1lem5  17638  pgpfaclem2  17641  pgpfaclem3  17642  ablfaclem3  17646  lcomfsupp  18054  psrbaglecl  18519  psrbagaddcl  18520  psrbagcon  18521  mplsubg  18587  mpllss  18588  mplcoe5  18618  psrbagsn  18644  psr1baslem  18704  dsmmfi  19223  dsmmacl  19226  dsmmsubg  19228  dsmmlss  19229  frlmsslsp  19276  mamures  19337  submabas  19525  mdetdiaglem  19545  mdetrlin  19549  mdetrsca  19550  mdetralt  19555  maducoeval2  19587  madugsum  19590  fctop  19941  restfpw  20117  fincmp  20330  cmpfi  20345  bwth  20347  finlocfin  20457  lfinpfin  20461  locfincmp  20463  1stckgenlem  20490  ptbasfi  20518  ptcnplem  20558  ptcmpfi  20750  cfinfil  20830  ufinffr  20866  fin1aufil  20869  tsmsres  21080  xrge0gsumle  21753  xrge0tsms  21754  fsumcn  21789  rrxcph  22235  rrxmval  22243  ovoliunlem1  22324  ovolicc2lem4  22342  ovolicc2lem5  22343  i1fima  22504  i1fd  22507  itg1cl  22511  itg1ge0  22512  i1f0  22513  i1f1  22516  i1fadd  22521  i1fmul  22522  itg1addlem4  22525  i1fmulc  22529  itg1mulc  22530  i1fres  22531  itg10a  22536  itg1ge0a  22537  itg1climres  22540  mbfi1fseqlem4  22544  itgfsum  22652  dvmptfsum  22795  plyexmo  23125  aannenlem2  23141  aalioulem2  23145  birthday  23736  jensenlem1  23768  jensenlem2  23769  jensen  23770  wilthlem2  23850  ppifi  23886  prmdvdsfi  23888  0sgm  23925  sgmf  23926  sgmnncl  23928  ppiprm  23932  chtprm  23934  chtdif  23939  efchtdvds  23940  ppidif  23944  ppiltx  23958  mumul  23962  sqff1o  23963  fsumdvdsdiag  23967  fsumdvdscom  23968  dvdsflsumcom  23971  musum  23974  musumsum  23975  muinv  23976  fsumdvdsmul  23978  ppiub  23986  vmasum  23998  logfac2  23999  perfectlem2  24012  dchrfi  24037  dchrabs  24042  dchrptlem1  24046  dchrptlem2  24047  dchrpt  24049  lgsquadlem1  24136  lgsquadlem2  24137  lgsquadlem3  24138  chebbnd1lem1  24161  chtppilimlem1  24165  rplogsumlem2  24177  rpvmasumlem  24179  dchrvmasumlem1  24187  dchrisum0ff  24199  rpvmasum2  24204  dchrisum0re  24205  dchrisum0  24212  rplogsum  24219  dirith2  24220  vmalogdivsum2  24230  logsqvma  24234  logsqvma2  24235  selberg  24240  selberg34r  24263  pntsval2  24268  pntrlog2bndlem1  24269  cusgrafi  25046  wwlknfi  25302  hashwwlkext  25310  clwwlknfi  25342  qerclwwlknfi  25393  vdgrfiun  25466  eupath2lem3  25543  konigsberg  25551  relfi  28043  imafi2  28122  unifi3  28123  ffsrn  28148  gsumle  28371  xrge0tsmsd  28378  hasheuni  28736  carsgclctunlem1  28969  sibfof  28992  sitgclg  28994  oddpwdc  29004  eulerpartlems  29010  eulerpartlemb  29018  eulerpartlemmf  29025  eulerpartlemgf  29029  eulerpartlemgs2  29030  coinfliplem  29128  coinflippv  29133  ballotlemfelz  29140  ballotlemfp1  29141  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemiex  29151  ballotlemsup  29154  ballotlemfg  29175  ballotlemfrc  29176  ballotlemfrceq  29178  ballotth  29187  deranglem  29668  subfacp1lem3  29684  subfacp1lem5  29686  subfacp1lem6  29687  erdszelem2  29694  erdszelem8  29700  erdsze2lem2  29706  snmlff  29831  mvrsfpw  29923  finminlem  30750  topdifinffinlem  31475  poimirlem9  31643  poimirlem26  31660  poimirlem27  31661  poimirlem28  31662  poimirlem30  31664  poimirlem32  31666  itg2addnclem2  31688  nnubfi  31773  nninfnub  31774  sstotbnd2  31800  cntotbnd  31822  rencldnfilem  35362  jm2.22  35546  jm2.23  35547  filnm  35644  phisum  35765  pwssfi  37011  disjinfi  37081  fsumiunss  37219  fprodexp  37236  fprodabs2  37237  mccllem  37239  sumnnodd  37272  fprodcncf  37341  dvmptfprod  37379  dvnprodlem1  37380  dvnprodlem2  37381  fourierdlem25  37553  fourierdlem37  37565  fourierdlem51  37579  fourierdlem79  37607  fouriersw  37653  etransclem16  37672  etransclem24  37680  etransclem33  37689  etransclem44  37700  sge0resplit  37772  sge0iunmptlemfi  37779  sge0iunmptlemre  37781  carageniuncllem2  37842  perfectALTVlem2  38224  rmsuppfi  38908  mndpsuppfi  38910  scmsuppfi  38912  suppmptcfin  38914
  Copyright terms: Public domain W3C validator