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

Theorem ssfi 7332
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 7134 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 7120 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5684 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5219 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5659 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3398 . . . . . . . . . . 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 7331 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 7134 . . . . . . . . . . 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 5676 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5692 . . . . . . . . . . . . . 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 2961 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 5189 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5668 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 3045 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 7120 . . . . . . . . . . . . . . 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 7162 . . . . . . . . . . . . . 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 2819 . . . . . . . . . 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 7134 . . . . . . . . . 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 1647 . . . . 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 2826 . . 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 1726   E.wrex 2708    C_ wss 3322   class class class wbr 4215   omcom 4848   ran crn 4882    |` cres 4883   "cima 4884   -1-1->wf1 5454   -onto->wfo 5455   -1-1-onto->wf1o 5456    ~~ cen 7109   Fincfn 7112
This theorem is referenced by:  domfi  7333  infi  7335  finresfin  7337  diffi  7342  findcard3  7353  unfir  7378  fnfi  7387  fofinf1o  7390  cnvfi  7393  f1fi  7396  imafi  7402  mapfi  7406  ixpfi  7407  ixpfi2  7408  mptfi  7409  elfiun  7438  marypha1lem  7441  wemapso2  7524  cantnfp1lem1  7637  oemapvali  7643  cantnflem1d  7647  cantnflem1  7648  mapfien  7656  ackbij2lem1  8104  ackbij1lem11  8115  fin23lem26  8210  fin23lem23  8211  fin23lem21  8224  fin11a  8268  isfin1-3  8271  axcclem  8342  pwfseqlem4  8542  hashun3  11663  hashssdif  11682  hashsslei  11690  hashbclem  11706  hashf1lem2  11710  seqcoll2  11718  isercolllem2  12464  isercoll  12466  fsumss  12524  fsum2dlem  12559  fsumcom2  12563  fsumless  12580  fsumabs  12585  fsumrlim  12595  fsumo1  12596  cvgcmpce  12602  fsumiun  12605  qshash  12611  incexclem  12621  incexc  12622  incexc2  12623  bitsfi  12954  bitsinv1  12959  bitsinvp1  12966  sadcaddlem  12974  sadadd2lem  12976  sadadd3  12978  sadaddlem  12983  sadasslem  12987  sadeq  12989  phicl2  13162  phibnd  13165  hashdvds  13169  phiprmpw  13170  phimullem  13173  eulerthlem2  13176  eulerth  13177  sumhash  13270  prmreclem2  13290  prmreclem3  13291  prmreclem4  13292  prmreclem5  13293  1arith  13300  4sqlem11  13328  vdwlem11  13364  hashbccl  13376  ramlb  13392  0ram  13393  ramub1lem1  13399  ramub1lem2  13400  isstruct2  13483  fisuppfi  14778  lagsubg2  15006  lagsubg  15007  orbsta2  15096  odcl2  15206  oddvds2  15207  sylow1lem2  15238  sylow1lem3  15239  sylow1lem4  15240  sylow1lem5  15241  odcau  15243  pgpssslw  15253  sylow2alem2  15257  sylow2a  15258  sylow2blem1  15259  sylow2blem3  15261  slwhash  15263  fislw  15264  sylow2  15265  sylow3lem1  15266  sylow3lem3  15268  sylow3lem4  15269  sylow3lem6  15271  cyggenod  15499  gsumval3  15519  gsumzadd  15532  gsumzsplit  15534  gsumzinv  15545  gsumsub  15547  gsumunsn  15549  gsumpt  15550  gsum2d  15551  gsum2d2lem  15552  dprdfid  15580  dprdfinv  15582  dprdfadd  15583  dprdsubg  15587  dmdprdsplitlem  15600  dpjidcl  15621  ablfacrplem  15628  ablfacrp2  15630  ablfac1c  15634  ablfac1eulem  15635  ablfac1eu  15636  pgpfac1lem5  15642  pgpfaclem2  15645  pgpfaclem3  15646  ablfaclem3  15650  psrbaglecl  16439  psrbagaddcl  16440  psrbagcon  16441  psrass1lem  16447  psrbas  16448  psrlidm  16472  psrridm  16473  psrass1  16474  psrdi  16475  psrdir  16476  psrcom  16477  psrass23  16478  mvridlem  16488  mplsubg  16505  mpllss  16506  mplsubrglem  16507  mplsubrg  16508  mvrcl  16517  mplmon  16531  mplmonmul  16532  mplcoe1  16533  mplcoe3  16534  mplcoe2  16535  mplbas2  16536  psrbagsn  16560  psrbagev1  16571  evlslem2  16573  psr1baslem  16588  psropprmul  16637  coe1mul2  16667  ply1coe  16689  fctop  17073  restfpw  17248  fincmp  17461  cmpfi  17476  1stckgenlem  17590  ptbasfi  17618  ptcnplem  17658  ptcmpfi  17850  cfinfil  17930  ufinffr  17966  fin1aufil  17969  tsms0  18176  tsmsres  18178  tgptsmscls  18184  xrge0gsumle  18869  xrge0tsms  18870  fsumcn  18905  ovoliunlem1  19403  ovolicc2lem4  19421  ovolicc2lem5  19422  i1fima  19573  i1fd  19576  itg1cl  19580  itg1ge0  19581  i1f0  19582  i1f1  19585  i1fadd  19590  i1fmul  19591  itg1addlem4  19594  i1fmulc  19598  itg1mulc  19599  i1fres  19600  itg10a  19605  itg1ge0a  19606  itg1climres  19609  mbfi1fseqlem4  19613  itgfsum  19721  dvmptfsum  19864  evlslem6  19939  evlslem3  19940  tdeglem4  19988  plypf1  20136  plyexmo  20235  aannenlem2  20251  aalioulem2  20255  tayl0  20283  birthday  20798  jensenlem1  20830  jensenlem2  20831  jensen  20832  wilthlem2  20857  ppifi  20893  prmdvdsfi  20895  0sgm  20932  sgmf  20933  sgmnncl  20935  ppiprm  20939  chtprm  20941  chtdif  20946  efchtdvds  20947  ppidif  20951  ppiltx  20965  mumul  20969  sqff1o  20970  fsumdvdsdiag  20974  fsumdvdscom  20975  dvdsflsumcom  20978  musum  20981  musumsum  20982  muinv  20983  fsumdvdsmul  20985  ppiub  20993  vmasum  21005  logfac2  21006  perfectlem2  21019  dchrfi  21044  dchrabs  21049  dchrptlem1  21053  dchrptlem2  21054  dchrptlem3  21055  dchrpt  21056  lgseisenlem3  21140  lgseisenlem4  21141  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  chebbnd1lem1  21168  chtppilimlem1  21172  rplogsumlem2  21184  rpvmasumlem  21186  dchrvmasumlem1  21194  dchrisum0ff  21206  rpvmasum2  21211  dchrisum0re  21212  dchrisum0  21219  rplogsum  21226  dirith2  21227  vmalogdivsum2  21237  logsqvma  21241  logsqvma2  21242  selberg  21247  selberg34r  21270  pntsval2  21275  pntrlog2bndlem1  21276  cusgrafi  21496  vdgrfiun  21678  eupath2lem3  21706  konigsberg  21714  xrge0tsmsd  24228  hasheuni  24480  sibfof  24659  sitgclg  24661  coinfliplem  24741  coinflippv  24746  ballotlemfelz  24753  ballotlemfp1  24754  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemiex  24764  ballotlemsup  24767  ballotlemfg  24788  ballotlemfrc  24789  ballotlemfrceq  24791  ballotth  24800  deranglem  24857  subfacp1lem3  24873  subfacp1lem5  24875  subfacp1lem6  24876  erdszelem2  24883  erdszelem8  24889  erdsze2lem2  24895  snmlff  25021  fprod2dlem  25309  fprodcom2  25313  itg2addnclem2  26271  finminlem  26335  finlocfin  26393  lfinpfin  26397  locfincmp  26398  nnubfi  26468  nninfnub  26469  sstotbnd2  26497  cntotbnd  26519  funsnfsup  26757  lcomfsup  26761  rencldnfilem  26895  jm2.22  27080  jm2.23  27081  filnm  27183  dsmmfi  27195  dsmmacl  27198  dsmmsubg  27200  dsmmlss  27201  uvcff  27231  uvcresum  27233  frlmsplit2  27234  frlmsslsp  27239  frlmup1  27241  symgfisg  27400  symggen2  27403  psgnghm2  27429  phisum  27509  hashss  28192
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 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
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 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-er 6908  df-en 7113  df-fin 7116
  Copyright terms: Public domain W3C validator