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

Theorem ssfi 7315
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 7117 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7103 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5667 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5202 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5642 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3383 . . . . . . . . . . 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 7314 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7117 . . . . . . . . . . 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 5659 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5675 . . . . . . . . . . . . . 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 2946 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5172 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5651 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 3030 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7103 . . . . . . . . . . . . . . 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 7145 . . . . . . . . . . . . . 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 2804 . . . . . . . . . 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 7117 . . . . . . . . . 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 1646 . . . . 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 2811 . . 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 1550    e. wcel 1725   E.wrex 2693    C_ wss 3307   class class class wbr 4199   omcom 4831   ran crn 4865    |` cres 4866   "cima 4867   -1-1->wf1 5437   -onto->wfo 5438   -1-1-onto->wf1o 5439    ~~ cen 7092   Fincfn 7095
This theorem is referenced by:  domfi  7316  infi  7318  finresfin  7320  diffi  7325  findcard3  7336  unfir  7361  fnfi  7370  fofinf1o  7373  cnvfi  7376  f1fi  7379  imafi  7385  mapfi  7389  ixpfi  7390  ixpfi2  7391  mptfi  7392  elfiun  7421  marypha1lem  7424  wemapso2  7505  cantnfp1lem1  7618  oemapvali  7624  cantnflem1d  7628  cantnflem1  7629  mapfien  7637  ackbij2lem1  8083  ackbij1lem11  8094  fin23lem26  8189  fin23lem23  8190  fin23lem21  8203  fin11a  8247  isfin1-3  8250  axcclem  8321  pwfseqlem4  8521  hashun3  11641  hashssdif  11660  hashsslei  11668  hashbclem  11684  hashf1lem2  11688  seqcoll2  11696  isercolllem2  12442  isercoll  12444  fsumss  12502  fsum2dlem  12537  fsumcom2  12541  fsumless  12558  fsumabs  12563  fsumrlim  12573  fsumo1  12574  cvgcmpce  12580  fsumiun  12583  qshash  12589  incexclem  12599  incexc  12600  incexc2  12601  bitsfi  12932  bitsinv1  12937  bitsinvp1  12944  sadcaddlem  12952  sadadd2lem  12954  sadadd3  12956  sadaddlem  12961  sadasslem  12965  sadeq  12967  phicl2  13140  phibnd  13143  hashdvds  13147  phiprmpw  13148  phimullem  13151  eulerthlem2  13154  eulerth  13155  sumhash  13248  prmreclem2  13268  prmreclem3  13269  prmreclem4  13270  prmreclem5  13271  1arith  13278  4sqlem11  13306  vdwlem11  13342  hashbccl  13354  ramlb  13370  0ram  13371  ramub1lem1  13377  ramub1lem2  13378  isstruct2  13461  fisuppfi  14756  lagsubg2  14984  lagsubg  14985  orbsta2  15074  odcl2  15184  oddvds2  15185  sylow1lem2  15216  sylow1lem3  15217  sylow1lem4  15218  sylow1lem5  15219  odcau  15221  pgpssslw  15231  sylow2alem2  15235  sylow2a  15236  sylow2blem1  15237  sylow2blem3  15239  slwhash  15241  fislw  15242  sylow2  15243  sylow3lem1  15244  sylow3lem3  15246  sylow3lem4  15247  sylow3lem6  15249  cyggenod  15477  gsumval3  15497  gsumzadd  15510  gsumzsplit  15512  gsumzinv  15523  gsumsub  15525  gsumunsn  15527  gsumpt  15528  gsum2d  15529  gsum2d2lem  15530  dprdfid  15558  dprdfinv  15560  dprdfadd  15561  dprdsubg  15565  dmdprdsplitlem  15578  dpjidcl  15599  ablfacrplem  15606  ablfacrp2  15608  ablfac1c  15612  ablfac1eulem  15613  ablfac1eu  15614  pgpfac1lem5  15620  pgpfaclem2  15623  pgpfaclem3  15624  ablfaclem3  15628  psrbaglecl  16417  psrbagaddcl  16418  psrbagcon  16419  psrass1lem  16425  psrbas  16426  psrlidm  16450  psrridm  16451  psrass1  16452  psrdi  16453  psrdir  16454  psrcom  16455  psrass23  16456  mvridlem  16466  mplsubg  16483  mpllss  16484  mplsubrglem  16485  mplsubrg  16486  mvrcl  16495  mplmon  16509  mplmonmul  16510  mplcoe1  16511  mplcoe3  16512  mplcoe2  16513  mplbas2  16514  psrbagsn  16538  psrbagev1  16549  evlslem2  16551  psr1baslem  16566  psropprmul  16615  coe1mul2  16645  ply1coe  16667  fctop  17051  restfpw  17226  fincmp  17439  cmpfi  17454  1stckgenlem  17568  ptbasfi  17596  ptcnplem  17636  ptcmpfi  17828  cfinfil  17908  ufinffr  17944  fin1aufil  17947  tsms0  18154  tsmsres  18156  tgptsmscls  18162  xrge0gsumle  18847  xrge0tsms  18848  fsumcn  18883  ovoliunlem1  19381  ovolicc2lem4  19399  ovolicc2lem5  19400  i1fima  19553  i1fd  19556  itg1cl  19560  itg1ge0  19561  i1f0  19562  i1f1  19565  i1fadd  19570  i1fmul  19571  itg1addlem4  19574  i1fmulc  19578  itg1mulc  19579  i1fres  19580  itg10a  19585  itg1ge0a  19586  itg1climres  19589  mbfi1fseqlem4  19593  itgfsum  19701  dvmptfsum  19842  evlslem6  19917  evlslem3  19918  tdeglem4  19966  plypf1  20114  plyexmo  20213  aannenlem2  20229  aalioulem2  20233  tayl0  20261  birthday  20776  jensenlem1  20808  jensenlem2  20809  jensen  20810  wilthlem2  20835  ppifi  20871  prmdvdsfi  20873  0sgm  20910  sgmf  20911  sgmnncl  20913  ppiprm  20917  chtprm  20919  chtdif  20924  efchtdvds  20925  ppidif  20929  ppiltx  20943  mumul  20947  sqff1o  20948  fsumdvdsdiag  20952  fsumdvdscom  20953  dvdsflsumcom  20956  musum  20959  musumsum  20960  muinv  20961  fsumdvdsmul  20963  ppiub  20971  vmasum  20983  logfac2  20984  perfectlem2  20997  dchrfi  21022  dchrabs  21027  dchrptlem1  21031  dchrptlem2  21032  dchrptlem3  21033  dchrpt  21034  lgseisenlem3  21118  lgseisenlem4  21119  lgsquadlem1  21121  lgsquadlem2  21122  lgsquadlem3  21123  chebbnd1lem1  21146  chtppilimlem1  21150  rplogsumlem2  21162  rpvmasumlem  21164  dchrvmasumlem1  21172  dchrisum0ff  21184  rpvmasum2  21189  dchrisum0re  21190  dchrisum0  21197  rplogsum  21204  dirith2  21205  vmalogdivsum2  21215  logsqvma  21219  logsqvma2  21220  selberg  21225  selberg34r  21248  pntsval2  21253  pntrlog2bndlem1  21254  cusgrafi  21474  vdgrfiun  21656  eupath2lem3  21684  konigsberg  21692  xrge0tsmsd  24206  hasheuni  24458  sibfof  24637  sitgclg  24639  coinfliplem  24719  coinflippv  24724  ballotlemfelz  24731  ballotlemfp1  24732  ballotlemfc0  24733  ballotlemfcc  24734  ballotlemiex  24742  ballotlemsup  24745  ballotlemfg  24766  ballotlemfrc  24767  ballotlemfrceq  24769  ballotth  24778  deranglem  24835  subfacp1lem3  24851  subfacp1lem5  24853  subfacp1lem6  24854  erdszelem2  24861  erdszelem8  24867  erdsze2lem2  24873  snmlff  24999  fprod2dlem  25288  fprodcom2  25292  itg2addnclem2  26198  finminlem  26253  finlocfin  26311  lfinpfin  26315  locfincmp  26316  nnubfi  26386  nninfnub  26387  sstotbnd2  26415  cntotbnd  26437  funsnfsup  26675  lcomfsup  26679  rencldnfilem  26813  jm2.22  26998  jm2.23  26999  filnm  27102  dsmmfi  27114  dsmmacl  27117  dsmmsubg  27119  dsmmlss  27120  uvcff  27150  uvcresum  27152  frlmsplit2  27153  frlmsslsp  27158  frlmup1  27160  symgfisg  27319  symggen2  27322  psgnghm2  27348  phisum  27428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-pss 3323  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-tp 3809  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-tr 4290  df-eprel 4481  df-id 4485  df-po 4490  df-so 4491  df-fr 4528  df-we 4530  df-ord 4571  df-on 4572  df-lim 4573  df-suc 4574  df-om 4832  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-fun 5442  df-fn 5443  df-f 5444  df-f1 5445  df-fo 5446  df-f1o 5447  df-er 6891  df-en 7096  df-fin 7099
  Copyright terms: Public domain W3C validator