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

Theorem ssfi 7258
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 7060 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7046 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5614 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5149 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5589 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3332 . . . . . . . . . . 11  |-  ( z : A -onto-> x  -> 
( z " B
)  C_  x )
73, 6syl 16 . . . . . . . . . 10  |-  ( z : A -1-1-onto-> x  ->  ( z
" B )  C_  x )
8 ssnnfi 7257 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7060 . . . . . . . . . . 11  |-  ( ( z " B )  e.  Fin  <->  E. y  e.  om  ( z " B )  ~~  y
)
108, 9sylib 189 . . . . . . . . . 10  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  E. y  e.  om  ( z " B
)  ~~  y )
117, 10sylan2 461 . . . . . . . . 9  |-  ( ( x  e.  om  /\  z : A -1-1-onto-> x )  ->  E. y  e.  om  ( z " B )  ~~  y
)
1211adantrr 698 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5606 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5622 . . . . . . . . . . . . . 14  |-  ( ( z : A -1-1-> x  /\  B  C_  A )  ->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) )
1513, 14sylan 458 . . . . . . . . . . . . 13  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( z  |`  B ) : B -1-1-onto-> ( z " B
) )
16 vex 2895 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5119 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5598 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 2979 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7046 . . . . . . . . . . . . . . 15  |-  ( B 
~~  ( z " B )  <->  E. x  x : B -1-1-onto-> ( z " B
) )
2119, 20sylibr 204 . . . . . . . . . . . . . 14  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  B  ~~  ( z " B
) )
22 entr 7088 . . . . . . . . . . . . . 14  |-  ( ( B  ~~  ( z
" B )  /\  ( z " B
)  ~~  y )  ->  B  ~~  y )
2321, 22sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2415, 23sylan 458 . . . . . . . . . . . 12  |-  ( ( ( z : A -1-1-onto-> x  /\  B  C_  A )  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2524ex 424 . . . . . . . . . . 11  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( ( z " B )  ~~  y  ->  B  ~~  y ) )
2625reximdv 2753 . . . . . . . . . 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 7060 . . . . . . . . . 10  |-  ( B  e.  Fin  <->  E. y  e.  om  B  ~~  y
)
2826, 27syl6ibr 219 . . . . . . . . 9  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  B  e.  Fin )
)
2928adantl 453 . . . . . . . 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 589 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1643 . . . . 5  |-  ( x  e.  om  ->  ( E. z  z : A
-1-1-onto-> x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
332, 32syl5bi 209 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
3433rexlimiv 2760 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C_  A  ->  B  e.  Fin ) )
351, 34sylbi 188 . 2  |-  ( A  e.  Fin  ->  ( B  C_  A  ->  B  e.  Fin ) )
3635imp 419 1  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547    e. wcel 1717   E.wrex 2643    C_ wss 3256   class class class wbr 4146   omcom 4778   ran crn 4812    |` cres 4813   "cima 4814   -1-1->wf1 5384   -onto->wfo 5385   -1-1-onto->wf1o 5386    ~~ cen 7035   Fincfn 7038
This theorem is referenced by:  domfi  7259  infi  7261  finresfin  7263  diffi  7268  findcard3  7279  unfir  7304  fnfi  7313  fofinf1o  7316  cnvfi  7319  f1fi  7322  imafi  7327  mapfi  7331  ixpfi  7332  ixpfi2  7333  mptfi  7334  elfiun  7363  marypha1lem  7366  wemapso2  7447  cantnfp1lem1  7560  oemapvali  7566  cantnflem1d  7570  cantnflem1  7571  mapfien  7579  ackbij2lem1  8025  ackbij1lem11  8036  fin23lem26  8131  fin23lem23  8132  fin23lem21  8145  fin11a  8189  isfin1-3  8192  axcclem  8263  pwfseqlem4  8463  hashun3  11578  hashssdif  11597  hashsslei  11605  hashbclem  11621  hashf1lem2  11625  seqcoll2  11633  isercolllem2  12379  isercoll  12381  fsumss  12439  fsum2dlem  12474  fsumcom2  12478  fsumless  12495  fsumabs  12500  fsumrlim  12510  fsumo1  12511  cvgcmpce  12517  fsumiun  12520  qshash  12526  incexclem  12536  incexc  12537  incexc2  12538  bitsfi  12869  bitsinv1  12874  bitsinvp1  12881  sadcaddlem  12889  sadadd2lem  12891  sadadd3  12893  sadaddlem  12898  sadasslem  12902  sadeq  12904  phicl2  13077  phibnd  13080  hashdvds  13084  phiprmpw  13085  phimullem  13088  eulerthlem2  13091  eulerth  13092  sumhash  13185  prmreclem2  13205  prmreclem3  13206  prmreclem4  13207  prmreclem5  13208  1arith  13215  4sqlem11  13243  vdwlem11  13279  hashbccl  13291  ramlb  13307  0ram  13308  ramub1lem1  13314  ramub1lem2  13315  isstruct2  13398  fisuppfi  14693  lagsubg2  14921  lagsubg  14922  orbsta2  15011  odcl2  15121  oddvds2  15122  sylow1lem2  15153  sylow1lem3  15154  sylow1lem4  15155  sylow1lem5  15156  odcau  15158  pgpssslw  15168  sylow2alem2  15172  sylow2a  15173  sylow2blem1  15174  sylow2blem3  15176  slwhash  15178  fislw  15179  sylow2  15180  sylow3lem1  15181  sylow3lem3  15183  sylow3lem4  15184  sylow3lem6  15186  cyggenod  15414  gsumval3  15434  gsumzadd  15447  gsumzsplit  15449  gsumzinv  15460  gsumsub  15462  gsumunsn  15464  gsumpt  15465  gsum2d  15466  gsum2d2lem  15467  dprdfid  15495  dprdfinv  15497  dprdfadd  15498  dprdsubg  15502  dmdprdsplitlem  15515  dpjidcl  15536  ablfacrplem  15543  ablfacrp2  15545  ablfac1c  15549  ablfac1eulem  15550  ablfac1eu  15551  pgpfac1lem5  15557  pgpfaclem2  15560  pgpfaclem3  15561  ablfaclem3  15565  psrbaglecl  16354  psrbagaddcl  16355  psrbagcon  16356  psrass1lem  16362  psrbas  16363  psrlidm  16387  psrridm  16388  psrass1  16389  psrdi  16390  psrdir  16391  psrcom  16392  psrass23  16393  mvridlem  16403  mplsubg  16420  mpllss  16421  mplsubrglem  16422  mplsubrg  16423  mvrcl  16432  mplmon  16446  mplmonmul  16447  mplcoe1  16448  mplcoe3  16449  mplcoe2  16450  mplbas2  16451  psrbagsn  16475  psrbagev1  16486  evlslem2  16488  psr1baslem  16503  psropprmul  16552  coe1mul2  16582  ply1coe  16604  fctop  16984  restfpw  17158  fincmp  17371  cmpfi  17386  1stckgenlem  17499  ptbasfi  17527  ptcnplem  17567  ptcmpfi  17759  cfinfil  17839  ufinffr  17875  fin1aufil  17878  tsms0  18085  tsmsres  18087  tgptsmscls  18093  xrge0gsumle  18728  xrge0tsms  18729  fsumcn  18764  ovoliunlem1  19258  ovolicc2lem4  19276  ovolicc2lem5  19277  i1fima  19430  i1fd  19433  itg1cl  19437  itg1ge0  19438  i1f0  19439  i1f1  19442  i1fadd  19447  i1fmul  19448  itg1addlem4  19451  i1fmulc  19455  itg1mulc  19456  i1fres  19457  itg10a  19462  itg1ge0a  19463  itg1climres  19466  mbfi1fseqlem4  19470  itgfsum  19578  dvmptfsum  19719  evlslem6  19794  evlslem3  19795  tdeglem4  19843  plypf1  19991  plyexmo  20090  aannenlem2  20106  aalioulem2  20110  tayl0  20138  birthday  20653  jensenlem1  20685  jensenlem2  20686  jensen  20687  wilthlem2  20712  ppifi  20748  prmdvdsfi  20750  0sgm  20787  sgmf  20788  sgmnncl  20790  ppiprm  20794  chtprm  20796  chtdif  20801  efchtdvds  20802  ppidif  20806  ppiltx  20820  mumul  20824  sqff1o  20825  fsumdvdsdiag  20829  fsumdvdscom  20830  dvdsflsumcom  20833  musum  20836  musumsum  20837  muinv  20838  fsumdvdsmul  20840  ppiub  20848  vmasum  20860  logfac2  20861  perfectlem2  20874  dchrfi  20899  dchrabs  20904  dchrptlem1  20908  dchrptlem2  20909  dchrptlem3  20910  dchrpt  20911  lgseisenlem3  20995  lgseisenlem4  20996  lgsquadlem1  20998  lgsquadlem2  20999  lgsquadlem3  21000  chebbnd1lem1  21023  chtppilimlem1  21027  rplogsumlem2  21039  rpvmasumlem  21041  dchrvmasumlem1  21049  dchrisum0ff  21061  rpvmasum2  21066  dchrisum0re  21067  dchrisum0  21074  rplogsum  21081  dirith2  21082  vmalogdivsum2  21092  logsqvma  21096  logsqvma2  21097  selberg  21102  selberg34r  21125  pntsval2  21130  pntrlog2bndlem1  21131  cusgrafi  21350  vdgrfiun  21514  eupath2lem3  21542  konigsberg  21550  xrge0tsmsd  24045  hasheuni  24264  coinfliplem  24508  coinflippv  24513  ballotlemfelz  24520  ballotlemfp1  24521  ballotlemfc0  24522  ballotlemfcc  24523  ballotlemiex  24531  ballotlemsup  24534  ballotlemfg  24555  ballotlemfrc  24556  ballotlemfrceq  24558  ballotth  24567  deranglem  24624  subfacp1lem3  24640  subfacp1lem5  24642  subfacp1lem6  24643  erdszelem2  24650  erdszelem8  24656  erdsze2lem2  24662  snmlff  24788  itg2addnclem2  25951  finminlem  26005  finlocfin  26063  lfinpfin  26067  locfincmp  26068  nnubfi  26138  nninfnub  26139  sstotbnd2  26167  cntotbnd  26189  funsnfsup  26427  lcomfsup  26431  rencldnfilem  26565  jm2.22  26750  jm2.23  26751  filnm  26854  dsmmfi  26866  dsmmacl  26869  dsmmsubg  26871  dsmmlss  26872  uvcff  26902  uvcresum  26904  frlmsplit2  26905  frlmsslsp  26910  frlmup1  26912  symgfisg  27071  symggen2  27074  psgnghm2  27100  phisum  27180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-sbc 3098  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-er 6834  df-en 7039  df-fin 7042
  Copyright terms: Public domain W3C validator