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

Theorem ssfi 7099
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 6901 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 6887 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5495 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5041 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5470 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3239 . . . . . . . . . . 11  |-  ( z : A -onto-> x  -> 
( z " B
)  C_  x )
73, 6syl 15 . . . . . . . . . 10  |-  ( z : A -1-1-onto-> x  ->  ( z
" B )  C_  x )
8 ssnnfi 7098 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 6901 . . . . . . . . . . 11  |-  ( ( z " B )  e.  Fin  <->  E. y  e.  om  ( z " B )  ~~  y
)
108, 9sylib 188 . . . . . . . . . 10  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  E. y  e.  om  ( z " B
)  ~~  y )
117, 10sylan2 460 . . . . . . . . 9  |-  ( ( x  e.  om  /\  z : A -1-1-onto-> x )  ->  E. y  e.  om  ( z " B )  ~~  y
)
1211adantrr 697 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5487 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5503 . . . . . . . . . . . . . 14  |-  ( ( z : A -1-1-> x  /\  B  C_  A )  ->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) )
1513, 14sylan 457 . . . . . . . . . . . . 13  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( z  |`  B ) : B -1-1-onto-> ( z " B
) )
16 vex 2804 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5011 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5479 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 2888 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 6887 . . . . . . . . . . . . . . 15  |-  ( B 
~~  ( z " B )  <->  E. x  x : B -1-1-onto-> ( z " B
) )
2119, 20sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  B  ~~  ( z " B
) )
22 entr 6929 . . . . . . . . . . . . . 14  |-  ( ( B  ~~  ( z
" B )  /\  ( z " B
)  ~~  y )  ->  B  ~~  y )
2321, 22sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2415, 23sylan 457 . . . . . . . . . . . 12  |-  ( ( ( z : A -1-1-onto-> x  /\  B  C_  A )  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2524ex 423 . . . . . . . . . . 11  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( ( z " B )  ~~  y  ->  B  ~~  y ) )
2625reximdv 2667 . . . . . . . . . 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 6901 . . . . . . . . . 10  |-  ( B  e.  Fin  <->  E. y  e.  om  B  ~~  y
)
2826, 27syl6ibr 218 . . . . . . . . 9  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  B  e.  Fin )
)
2928adantl 452 . . . . . . . 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 14 . . . . . . 7  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  B  e.  Fin )
3130exp32 588 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1626 . . . . 5  |-  ( x  e.  om  ->  ( E. z  z : A
-1-1-onto-> x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
332, 32syl5bi 208 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
3433rexlimiv 2674 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C_  A  ->  B  e.  Fin ) )
351, 34sylbi 187 . 2  |-  ( A  e.  Fin  ->  ( B  C_  A  ->  B  e.  Fin ) )
3635imp 418 1  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531    e. wcel 1696   E.wrex 2557    C_ wss 3165   class class class wbr 4039   omcom 4672   ran crn 4706    |` cres 4707   "cima 4708   -1-1->wf1 5268   -onto->wfo 5269   -1-1-onto->wf1o 5270    ~~ cen 6876   Fincfn 6879
This theorem is referenced by:  domfi  7100  diffi  7105  findcard3  7116  unfir  7141  fnfi  7150  fofinf1o  7153  fidomdm  7154  cnvfi  7156  f1fi  7159  imafi  7164  mapfi  7168  ixpfi  7169  ixpfi2  7170  mptfi  7171  elfiun  7199  marypha1lem  7202  wemapso2  7283  cantnfp1lem1  7396  oemapvali  7402  cantnflem1d  7406  cantnflem1  7407  mapfien  7415  ackbij2lem1  7861  ackbij1lem11  7872  fin23lem26  7967  fin23lem23  7968  fin23lem22  7969  fin23lem21  7981  fin11a  8025  isfin1-3  8028  axcclem  8099  pwfseqlem4  8300  hashun3  11382  hashssdif  11390  hashsslei  11394  hashbclem  11406  hashf1lem2  11410  seqcoll2  11418  isercolllem2  12155  isercoll  12157  fsumss  12214  fsum2dlem  12249  fsumcom2  12253  fsumless  12270  fsumabs  12275  fsumrlim  12285  fsumo1  12286  cvgcmpce  12292  fsumiun  12295  qshash  12301  incexclem  12311  incexc  12312  incexc2  12313  bitsfi  12644  bitsinv1  12649  bitsinvp1  12656  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  phicl2  12852  phibnd  12855  hashdvds  12859  phiprmpw  12860  phimullem  12863  eulerthlem2  12866  eulerth  12867  sumhash  12960  prmreclem2  12980  prmreclem3  12981  prmreclem4  12982  prmreclem5  12983  1arith  12990  4sqlem11  13018  vdwlem11  13054  hashbccl  13066  ramlb  13082  0ram  13083  ramub1lem1  13089  ramub1lem2  13090  isstruct2  13173  fisuppfi  14466  lagsubg2  14694  lagsubg  14695  orbsta2  14784  odcl2  14894  oddvds2  14895  sylow1lem2  14926  sylow1lem3  14927  sylow1lem4  14928  sylow1lem5  14929  odcau  14931  pgpssslw  14941  sylow2alem2  14945  sylow2a  14946  sylow2blem1  14947  sylow2blem3  14949  slwhash  14951  fislw  14952  sylow2  14953  sylow3lem1  14954  sylow3lem3  14956  sylow3lem4  14957  sylow3lem6  14959  cyggenod  15187  gsumval3  15207  gsumzadd  15220  gsumzsplit  15222  gsumzinv  15233  gsumsub  15235  gsumunsn  15237  gsumpt  15238  gsum2d  15239  gsum2d2lem  15240  dprdfid  15268  dprdfinv  15270  dprdfadd  15271  dprdsubg  15275  dmdprdsplitlem  15288  dpjidcl  15309  ablfacrplem  15316  ablfacrp2  15318  ablfac1c  15322  ablfac1eulem  15323  ablfac1eu  15324  pgpfac1lem5  15330  pgpfaclem2  15333  pgpfaclem3  15334  ablfaclem3  15338  psrbaglecl  16131  psrbagaddcl  16132  psrbagcon  16133  psrass1lem  16139  psrbas  16140  psrlidm  16164  psrridm  16165  psrass1  16166  psrdi  16167  psrdir  16168  psrcom  16169  psrass23  16170  mvridlem  16180  mplsubg  16197  mpllss  16198  mplsubrglem  16199  mplsubrg  16200  mvrcl  16209  mplmon  16223  mplmonmul  16224  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  mplbas2  16228  psrbagsn  16252  psrbagev1  16263  evlslem2  16265  psr1baslem  16280  psropprmul  16332  coe1mul2  16362  ply1coe  16384  fctop  16757  restfpw  16926  fincmp  17136  cmpfi  17151  1stckgenlem  17264  ptbasfi  17292  ptcnplem  17331  ptcmpfi  17520  cfinfil  17604  ufinffr  17640  fin1aufil  17643  tsms0  17840  tsmsres  17842  tgptsmscls  17848  xrge0gsumle  18354  xrge0tsms  18355  fsumcn  18390  ovoliunlem1  18877  ovolicc2lem4  18895  ovolicc2lem5  18896  i1fima  19049  i1fd  19052  itg1cl  19056  itg1ge0  19057  i1f0  19058  i1f1  19061  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  i1fmulc  19074  itg1mulc  19075  i1fres  19076  itg10a  19081  itg1ge0a  19082  itg1climres  19085  mbfi1fseqlem4  19089  itgfsum  19197  dvmptfsum  19338  evlslem6  19413  evlslem3  19414  tdeglem4  19462  plypf1  19610  plyexmo  19709  aannenlem2  19725  aalioulem2  19729  tayl0  19757  birthday  20265  jensenlem1  20297  jensenlem2  20298  jensen  20299  wilthlem2  20323  ppifi  20359  prmdvdsfi  20361  0sgm  20398  sgmf  20399  sgmnncl  20401  ppiprm  20405  chtprm  20407  chtdif  20412  efchtdvds  20413  ppidif  20417  ppiltx  20431  mumul  20435  sqff1o  20436  fsumdvdsdiag  20440  fsumdvdscom  20441  dvdsflsumcom  20444  musum  20447  musumsum  20448  muinv  20449  fsumdvdsmul  20451  ppiub  20459  vmasum  20471  logfac2  20472  perfectlem2  20485  dchrfi  20510  dchrabs  20515  dchrptlem1  20519  dchrptlem2  20520  dchrptlem3  20521  dchrpt  20522  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  chebbnd1lem1  20634  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasumlem  20652  dchrvmasumlem1  20660  dchrisum0ff  20672  rpvmasum2  20677  dchrisum0re  20678  dchrisum0  20685  rplogsum  20692  dirith2  20693  vmalogdivsum2  20703  logsqvma  20707  logsqvma2  20708  selberg  20713  selberg34r  20736  pntsval2  20741  pntrlog2bndlem1  20742  infi  23045  ballotlemfelz  23065  ballotlemfp1  23066  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemiex  23076  ballotlemsup  23079  ballotlemfg  23100  ballotlemfrc  23101  ballotlemfrceq  23103  ballotth  23112  infi1  23185  xrge0tsmsd  23397  hasheuni  23468  coinfliplem  23694  coinflippv  23699  deranglem  23712  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  erdszelem2  23738  erdszelem8  23744  erdsze2lem2  23750  vdgrf  23906  vdgrun  23908  eupath2lem3  23918  konigsberg  23926  snmlff  23927  itg2addnclem2  25004  unfinsef  25172  stfincomp  25694  finminlem  26334  finptfin  26400  finlocfin  26402  lfinpfin  26406  locfincmp  26407  nnubfi  26563  nninfnub  26564  sstotbnd2  26601  sstotbnd3  26603  cntotbnd  26623  funsnfsup  26865  lcomfsup  26871  rencldnfilem  27006  jm2.22  27191  jm2.23  27192  filnm  27295  dsmmfi  27307  dsmmacl  27310  dsmmsubg  27312  dsmmlss  27313  uvcff  27343  uvcresum  27345  frlmsplit2  27346  frlmsslsp  27351  frlmup1  27353  symgfisg  27512  symggen2  27515  psgnghm2  27541  phisum  27621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-er 6676  df-en 6880  df-fin 6883
  Copyright terms: Public domain W3C validator