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

Theorem ssfi 7634
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 7433 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7419 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5746 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5278 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5721 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3502 . . . . . . . . . . 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 7633 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7433 . . . . . . . . . . 11  |-  ( ( z " B )  e.  Fin  <->  E. y  e.  om  ( z " B )  ~~  y
)
108, 9sylib 196 . . . . . . . . . 10  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  E. y  e.  om  ( z " B
)  ~~  y )
117, 10sylan2 474 . . . . . . . . 9  |-  ( ( x  e.  om  /\  z : A -1-1-onto-> x )  ->  E. y  e.  om  ( z " B )  ~~  y
)
1211adantrr 716 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5738 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5753 . . . . . . . . . . . . . 14  |-  ( ( z : A -1-1-> x  /\  B  C_  A )  ->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) )
1513, 14sylan 471 . . . . . . . . . . . . 13  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( z  |`  B ) : B -1-1-onto-> ( z " B
) )
16 vex 3071 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5248 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5730 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 3160 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7419 . . . . . . . . . . . . . . 15  |-  ( B 
~~  ( z " B )  <->  E. x  x : B -1-1-onto-> ( z " B
) )
2119, 20sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  B  ~~  ( z " B
) )
22 entr 7461 . . . . . . . . . . . . . 14  |-  ( ( B  ~~  ( z
" B )  /\  ( z " B
)  ~~  y )  ->  B  ~~  y )
2321, 22sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2415, 23sylan 471 . . . . . . . . . . . 12  |-  ( ( ( z : A -1-1-onto-> x  /\  B  C_  A )  /\  ( z " B )  ~~  y
)  ->  B  ~~  y )
2524ex 434 . . . . . . . . . . 11  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( ( z " B )  ~~  y  ->  B  ~~  y ) )
2625reximdv 2923 . . . . . . . . . 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 7433 . . . . . . . . . 10  |-  ( B  e.  Fin  <->  E. y  e.  om  B  ~~  y
)
2826, 27syl6ibr 227 . . . . . . . . 9  |-  ( ( z : A -1-1-onto-> x  /\  B  C_  A )  -> 
( E. y  e. 
om  ( z " B )  ~~  y  ->  B  e.  Fin )
)
2928adantl 466 . . . . . . . 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 605 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1691 . . . . 5  |-  ( x  e.  om  ->  ( E. z  z : A
-1-1-onto-> x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
332, 32syl5bi 217 . . . 4  |-  ( x  e.  om  ->  ( A  ~~  x  ->  ( B  C_  A  ->  B  e.  Fin ) ) )
3433rexlimiv 2931 . . 3  |-  ( E. x  e.  om  A  ~~  x  ->  ( B 
C_  A  ->  B  e.  Fin ) )
351, 34sylbi 195 . 2  |-  ( A  e.  Fin  ->  ( B  C_  A  ->  B  e.  Fin ) )
3635imp 429 1  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1587    e. wcel 1758   E.wrex 2796    C_ wss 3426   class class class wbr 4390   ran crn 4939    |` cres 4940   "cima 4941   -1-1->wf1 5513   -onto->wfo 5514   -1-1-onto->wf1o 5515   omcom 6576    ~~ cen 7407   Fincfn 7410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-om 6577  df-er 7201  df-en 7411  df-fin 7414
This theorem is referenced by:  domfi  7635  infi  7637  finresfin  7639  diffi  7644  findcard3  7656  unfir  7681  fnfi  7690  fofinf1o  7693  cnvfi  7696  f1fi  7699  imafi  7705  mapfi  7708  ixpfi  7709  ixpfi2  7710  mptfi  7711  cnvimamptfin  7713  fisuppfi  7729  suppssfifsupp  7736  fsuppunbi  7742  snopfsupp  7744  fsuppres  7746  ressuppfi  7747  fsuppmptif  7750  fsuppco2  7753  fsuppcor  7754  sniffsupp  7760  elfiun  7781  marypha1lem  7784  wemapso2OLD  7867  wemapso2lem  7868  cantnfp1lem1  7987  oemapvali  7993  cantnfp1lem1OLD  8013  cantnflem1dOLD  8020  cantnflem1OLD  8021  mapfienOLD  8028  ackbij2lem1  8489  ackbij1lem11  8500  fin23lem26  8595  fin23lem23  8596  fin23lem21  8609  fin11a  8653  isfin1-3  8656  axcclem  8727  pwfseqlem4  8930  hashun3  12249  hashss  12268  hashssdif  12269  hashsslei  12278  pr2pwpr  12285  hashbclem  12307  hashf1lem2  12311  seqcoll2  12319  isercolllem2  13245  isercoll  13247  fsumss  13304  fsum2dlem  13339  fsumcom2  13343  fsumless  13361  fsumabs  13366  fsumrlim  13376  fsumo1  13377  cvgcmpce  13383  fsumiun  13386  qshash  13392  incexclem  13401  incexc  13402  incexc2  13403  bitsfi  13735  bitsinv1  13740  bitsinvp1  13747  sadcaddlem  13755  sadadd2lem  13757  sadadd3  13759  sadaddlem  13764  sadasslem  13768  sadeq  13770  phicl2  13945  phibnd  13948  hashdvds  13952  phiprmpw  13953  phimullem  13956  eulerthlem2  13959  eulerth  13960  sumhash  14060  prmreclem2  14080  prmreclem3  14081  prmreclem4  14082  prmreclem5  14083  1arith  14090  4sqlem11  14118  vdwlem11  14154  hashbccl  14166  ramlb  14182  0ram  14183  ramub1lem1  14189  ramub1lem2  14190  isstruct2  14285  lagsubg2  15844  lagsubg  15845  orbsta2  15934  symgbasfi  15993  symgfisg  16076  symggen2  16079  odcl2  16170  oddvds2  16171  sylow1lem2  16202  sylow1lem3  16203  sylow1lem4  16204  sylow1lem5  16205  odcau  16207  pgpssslw  16217  sylow2alem2  16221  sylow2a  16222  sylow2blem1  16223  sylow2blem3  16225  slwhash  16227  fislw  16228  sylow2  16229  sylow3lem1  16230  sylow3lem3  16232  sylow3lem4  16233  sylow3lem6  16235  cyggenod  16465  gsumval3OLD  16486  gsumval3lem1  16487  gsumval3lem2  16488  gsumval3  16489  gsumzadd  16513  gsumzaddOLD  16515  gsumzsplitOLD  16523  gsumzinvOLD  16548  gsumsubOLD  16553  gsumpt  16559  gsumptOLD  16560  gsum2dlem1  16566  gsum2dlem2  16567  gsum2d  16568  gsum2dOLD  16569  gsum2d2lem  16570  dprdfadd  16615  dprdfidOLD  16619  dprdfinvOLD  16621  dprdfaddOLD  16622  dmdprdsplitlemOLD  16640  dpjidclOLD  16669  ablfacrplem  16671  ablfacrp2  16673  ablfac1c  16677  ablfac1eulem  16678  ablfac1eu  16679  pgpfac1lem5  16685  pgpfaclem2  16688  pgpfaclem3  16689  ablfaclem3  16693  lcomfsupOLD  17090  lcomfsupp  17091  psrbaglecl  17543  psrbagaddcl  17544  psrbagaddclOLD  17545  psrbagcon  17546  psrbasOLD  17555  psrlidmOLD  17581  psrridmOLD  17583  mvridlemOLD  17599  mplsubg  17622  mpllss  17623  mplsubrglemOLD  17625  mplcoe3OLD  17653  mplcoe5  17655  mplcoe2OLD  17657  mplbas2OLD  17659  psrbagsn  17684  psrbagev1OLD  17702  evlslem6OLD  17706  psr1baslem  17748  funsnfsupOLD  17777  psgnghm2  18120  dsmmfi  18272  dsmmacl  18275  dsmmsubg  18277  dsmmlss  18278  frlmsslsp  18332  frlmsslspOLD  18333  mamures  18399  submabas  18500  mdetdiaglem  18520  mdetrlin  18524  mdetrsca  18525  mdetralt  18530  maducoeval2  18562  madugsum  18565  fctop  18724  restfpw  18899  fincmp  19112  cmpfi  19127  bwth  19129  1stckgenlem  19242  ptbasfi  19270  ptcnplem  19310  ptcmpfi  19502  cfinfil  19582  ufinffr  19618  fin1aufil  19621  tsmsresOLD  19833  tsmsres  19834  xrge0gsumle  20526  xrge0tsms  20527  fsumcn  20562  rrxcph  21012  rrxmval  21020  ovoliunlem1  21101  ovolicc2lem4  21119  ovolicc2lem5  21120  i1fima  21272  i1fd  21275  itg1cl  21279  itg1ge0  21280  i1f0  21281  i1f1  21284  i1fadd  21289  i1fmul  21290  itg1addlem4  21293  i1fmulc  21297  itg1mulc  21298  i1fres  21299  itg10a  21304  itg1ge0a  21305  itg1climres  21308  mbfi1fseqlem4  21312  itgfsum  21420  dvmptfsum  21563  plyexmo  21895  aannenlem2  21911  aalioulem2  21915  birthday  22464  jensenlem1  22496  jensenlem2  22497  jensen  22498  wilthlem2  22523  ppifi  22559  prmdvdsfi  22561  0sgm  22598  sgmf  22599  sgmnncl  22601  ppiprm  22605  chtprm  22607  chtdif  22612  efchtdvds  22613  ppidif  22617  ppiltx  22631  mumul  22635  sqff1o  22636  fsumdvdsdiag  22640  fsumdvdscom  22641  dvdsflsumcom  22644  musum  22647  musumsum  22648  muinv  22649  fsumdvdsmul  22651  ppiub  22659  vmasum  22671  logfac2  22672  perfectlem2  22685  dchrfi  22710  dchrabs  22715  dchrptlem1  22719  dchrptlem2  22720  dchrpt  22722  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  chebbnd1lem1  22834  chtppilimlem1  22838  rplogsumlem2  22850  rpvmasumlem  22852  dchrvmasumlem1  22860  dchrisum0ff  22872  rpvmasum2  22877  dchrisum0re  22878  dchrisum0  22885  rplogsum  22892  dirith2  22893  vmalogdivsum2  22903  logsqvma  22907  logsqvma2  22908  selberg  22913  selberg34r  22936  pntsval2  22941  pntrlog2bndlem1  22942  cusgrafi  23525  vdgrfiun  23707  eupath2lem3  23735  konigsberg  23743  relfi  26074  unifi3  26139  ffsrn  26163  gsumunsnf  26379  gsumle  26380  xrge0tsmsd  26387  hasheuni  26668  sibfof  26860  sitgclg  26862  oddpwdc  26871  eulerpartlems  26877  eulerpartlemb  26885  eulerpartlemmf  26892  eulerpartlemgf  26896  eulerpartlemgs2  26897  coinfliplem  26995  coinflippv  27000  ballotlemfelz  27007  ballotlemfp1  27008  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemiex  27018  ballotlemsup  27021  ballotlemfg  27042  ballotlemfrc  27043  ballotlemfrceq  27045  ballotth  27054  deranglem  27188  subfacp1lem3  27204  subfacp1lem5  27206  subfacp1lem6  27207  erdszelem2  27214  erdszelem8  27220  erdsze2lem2  27226  snmlff  27352  fprod2dlem  27625  fprodcom2  27629  itg2addnclem2  28582  finminlem  28651  finlocfin  28709  lfinpfin  28713  locfincmp  28714  nnubfi  28784  nninfnub  28785  sstotbnd2  28811  cntotbnd  28833  rencldnfilem  29297  jm2.22  29482  jm2.23  29483  filnm  29581  phisum  29705  wwlknfi  30508  clwwlknfi  30615  qerclwwlknfi  30641  hashwwlkext  30703  ssnn0fi  30884  rmsuppfi  30925  mndpsuppfi  30927  scmsuppfi  30929  suppmptcfin  30931
  Copyright terms: Public domain W3C validator