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

Theorem ssfi 7365
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 7167 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7153 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5716 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5249 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5691 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3385 . . . . . . . . . . 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 7364 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7167 . . . . . . . . . . 11  |-  ( ( z " B )  e.  Fin  <->  E. y  e.  om  ( z " B )  ~~  y
)
108, 9sylib 190 . . . . . . . . . 10  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  E. y  e.  om  ( z " B
)  ~~  y )
117, 10sylan2 462 . . . . . . . . 9  |-  ( ( x  e.  om  /\  z : A -1-1-onto-> x )  ->  E. y  e.  om  ( z " B )  ~~  y
)
1211adantrr 699 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5708 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5724 . . . . . . . . . . . . . 14  |-  ( ( z : A -1-1-> x  /\  B  C_  A )  ->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) )
1513, 14sylan 459 . . . . . . . . . . . . 13  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( z  |`  B ) : B -1-1-onto-> ( z " B
) )
16 vex 2968 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5221 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5700 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 3052 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7153 . . . . . . . . . . . . . . 15  |-  ( B 
~~  ( z " B )  <->  E. x  x : B -1-1-onto-> ( z " B
) )
2119, 20sylibr 205 . . . . . . . . . . . . . 14  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  B  ~~  ( z " B
) )
22 entr 7195 . . . . . . . . . . . . . 14  |-  ( ( B  ~~  ( z
" B )  /\  ( z " B
)  ~~  y )  ->  B  ~~  y )
2321, 22sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2415, 23sylan 459 . . . . . . . . . . . 12  |-  ( ( ( z : A -1-1-onto-> x  /\  B  C_  A )  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2524ex 425 . . . . . . . . . . 11  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( ( z " B )  ~~  y  ->  B  ~~  y ) )
2625reximdv 2824 . . . . . . . . . 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 7167 . . . . . . . . . 10  |-  ( B  e.  Fin  <->  E. y  e.  om  B  ~~  y
)
2826, 27syl6ibr 220 . . . . . . . . 9  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  B  e.  Fin )
)
2928adantl 454 . . . . . . . 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 590 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1648 . . . . 5  |-  ( x  e.  om  ->  ( E. z  z : A
-1-1-onto-> x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
332, 32syl5bi 210 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
3433rexlimiv 2831 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C_  A  ->  B  e.  Fin ) )
351, 34sylbi 189 . 2  |-  ( A  e.  Fin  ->  ( B  C_  A  ->  B  e.  Fin ) )
3635imp 420 1  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551    e. wcel 1728   E.wrex 2713    C_ wss 3309   class class class wbr 4243   omcom 4880   ran crn 4914    |` cres 4915   "cima 4916   -1-1->wf1 5486   -onto->wfo 5487   -1-1-onto->wf1o 5488    ~~ cen 7142   Fincfn 7145
This theorem is referenced by:  domfi  7366  infi  7368  finresfin  7370  diffi  7375  findcard3  7386  unfir  7411  fnfi  7420  fofinf1o  7423  cnvfi  7426  f1fi  7429  imafi  7435  mapfi  7439  ixpfi  7440  ixpfi2  7441  mptfi  7442  elfiun  7471  marypha1lem  7474  wemapso2  7557  cantnfp1lem1  7670  oemapvali  7676  cantnflem1d  7680  cantnflem1  7681  mapfien  7689  ackbij2lem1  8137  ackbij1lem11  8148  fin23lem26  8243  fin23lem23  8244  fin23lem21  8257  fin11a  8301  isfin1-3  8304  axcclem  8375  pwfseqlem4  8575  hashun3  11696  hashssdif  11715  hashsslei  11723  hashbclem  11739  hashf1lem2  11743  seqcoll2  11751  isercolllem2  12497  isercoll  12499  fsumss  12557  fsum2dlem  12592  fsumcom2  12596  fsumless  12613  fsumabs  12618  fsumrlim  12628  fsumo1  12629  cvgcmpce  12635  fsumiun  12638  qshash  12644  incexclem  12654  incexc  12655  incexc2  12656  bitsfi  12987  bitsinv1  12992  bitsinvp1  12999  sadcaddlem  13007  sadadd2lem  13009  sadadd3  13011  sadaddlem  13016  sadasslem  13020  sadeq  13022  phicl2  13195  phibnd  13198  hashdvds  13202  phiprmpw  13203  phimullem  13206  eulerthlem2  13209  eulerth  13210  sumhash  13303  prmreclem2  13323  prmreclem3  13324  prmreclem4  13325  prmreclem5  13326  1arith  13333  4sqlem11  13361  vdwlem11  13397  hashbccl  13409  ramlb  13425  0ram  13426  ramub1lem1  13432  ramub1lem2  13433  isstruct2  13516  fisuppfi  14811  lagsubg2  15039  lagsubg  15040  orbsta2  15129  odcl2  15239  oddvds2  15240  sylow1lem2  15271  sylow1lem3  15272  sylow1lem4  15273  sylow1lem5  15274  odcau  15276  pgpssslw  15286  sylow2alem2  15290  sylow2a  15291  sylow2blem1  15292  sylow2blem3  15294  slwhash  15296  fislw  15297  sylow2  15298  sylow3lem1  15299  sylow3lem3  15301  sylow3lem4  15302  sylow3lem6  15304  cyggenod  15532  gsumval3  15552  gsumzadd  15565  gsumzsplit  15567  gsumzinv  15578  gsumsub  15580  gsumunsn  15582  gsumpt  15583  gsum2d  15584  gsum2d2lem  15585  dprdfid  15613  dprdfinv  15615  dprdfadd  15616  dprdsubg  15620  dmdprdsplitlem  15633  dpjidcl  15654  ablfacrplem  15661  ablfacrp2  15663  ablfac1c  15667  ablfac1eulem  15668  ablfac1eu  15669  pgpfac1lem5  15675  pgpfaclem2  15678  pgpfaclem3  15679  ablfaclem3  15683  psrbaglecl  16472  psrbagaddcl  16473  psrbagcon  16474  psrass1lem  16480  psrbas  16481  psrlidm  16505  psrridm  16506  psrass1  16507  psrdi  16508  psrdir  16509  psrcom  16510  psrass23  16511  mvridlem  16521  mplsubg  16538  mpllss  16539  mplsubrglem  16540  mplsubrg  16541  mvrcl  16550  mplmon  16564  mplmonmul  16565  mplcoe1  16566  mplcoe3  16567  mplcoe2  16568  mplbas2  16569  psrbagsn  16593  psrbagev1  16604  evlslem2  16606  psr1baslem  16621  psropprmul  16670  coe1mul2  16700  ply1coe  16722  fctop  17106  restfpw  17281  fincmp  17494  cmpfi  17509  1stckgenlem  17623  ptbasfi  17651  ptcnplem  17691  ptcmpfi  17883  cfinfil  17963  ufinffr  17999  fin1aufil  18002  tsms0  18209  tsmsres  18211  tgptsmscls  18217  xrge0gsumle  18902  xrge0tsms  18903  fsumcn  18938  ovoliunlem1  19436  ovolicc2lem4  19454  ovolicc2lem5  19455  i1fima  19606  i1fd  19609  itg1cl  19613  itg1ge0  19614  i1f0  19615  i1f1  19618  i1fadd  19623  i1fmul  19624  itg1addlem4  19627  i1fmulc  19631  itg1mulc  19632  i1fres  19633  itg10a  19638  itg1ge0a  19639  itg1climres  19642  mbfi1fseqlem4  19646  itgfsum  19754  dvmptfsum  19897  evlslem6  19972  evlslem3  19973  tdeglem4  20021  plypf1  20169  plyexmo  20268  aannenlem2  20284  aalioulem2  20288  tayl0  20316  birthday  20831  jensenlem1  20863  jensenlem2  20864  jensen  20865  wilthlem2  20890  ppifi  20926  prmdvdsfi  20928  0sgm  20965  sgmf  20966  sgmnncl  20968  ppiprm  20972  chtprm  20974  chtdif  20979  efchtdvds  20980  ppidif  20984  ppiltx  20998  mumul  21002  sqff1o  21003  fsumdvdsdiag  21007  fsumdvdscom  21008  dvdsflsumcom  21011  musum  21014  musumsum  21015  muinv  21016  fsumdvdsmul  21018  ppiub  21026  vmasum  21038  logfac2  21039  perfectlem2  21052  dchrfi  21077  dchrabs  21082  dchrptlem1  21086  dchrptlem2  21087  dchrptlem3  21088  dchrpt  21089  lgseisenlem3  21173  lgseisenlem4  21174  lgsquadlem1  21176  lgsquadlem2  21177  lgsquadlem3  21178  chebbnd1lem1  21201  chtppilimlem1  21205  rplogsumlem2  21217  rpvmasumlem  21219  dchrvmasumlem1  21227  dchrisum0ff  21239  rpvmasum2  21244  dchrisum0re  21245  dchrisum0  21252  rplogsum  21259  dirith2  21260  vmalogdivsum2  21270  logsqvma  21274  logsqvma2  21275  selberg  21280  selberg34r  21303  pntsval2  21308  pntrlog2bndlem1  21309  cusgrafi  21529  vdgrfiun  21711  eupath2lem3  21739  konigsberg  21747  xrge0tsmsd  24258  hasheuni  24510  sibfof  24689  sitgclg  24691  coinfliplem  24771  coinflippv  24776  ballotlemfelz  24783  ballotlemfp1  24784  ballotlemfc0  24785  ballotlemfcc  24786  ballotlemiex  24794  ballotlemsup  24797  ballotlemfg  24818  ballotlemfrc  24819  ballotlemfrceq  24821  ballotth  24830  deranglem  24887  subfacp1lem3  24903  subfacp1lem5  24905  subfacp1lem6  24906  erdszelem2  24913  erdszelem8  24919  erdsze2lem2  24925  snmlff  25051  fprod2dlem  25339  fprodcom2  25343  itg2addnclem2  26299  finminlem  26363  finlocfin  26421  lfinpfin  26425  locfincmp  26426  nnubfi  26496  nninfnub  26497  sstotbnd2  26525  cntotbnd  26547  funsnfsup  26855  lcomfsup  26859  rencldnfilem  26993  jm2.22  27178  jm2.23  27179  filnm  27281  dsmmfi  27293  dsmmacl  27296  dsmmsubg  27298  dsmmlss  27299  uvcff  27329  uvcresum  27331  frlmsplit2  27332  frlmsslsp  27337  frlmup1  27339  symgfisg  27498  symggen2  27501  psgnghm2  27527  phisum  27607  hashss  28290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-er 6941  df-en 7146  df-fin 7149
  Copyright terms: Public domain W3C validator