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

Theorem ssfi 6968
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
StepHypRef Expression
1 isfi 6771 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 6757 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5336 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 4932 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5311 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3147 . . . . . . . . . . 11  |-  ( z : A -onto-> x  -> 
( z " B
)  C_  x )
73, 6syl 17 . . . . . . . . . 10  |-  ( z : A -1-1-onto-> x  ->  ( z
" B )  C_  x )
8 ssnnfi 6967 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 6771 . . . . . . . . . . 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 700 . . . . . . . 8  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  E. y  e.  om  ( z " B )  ~~  y
)
13 f1of1 5328 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5344 . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 4902 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5320 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18cla4ev 2812 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 6757 . . . . . . . . . . . . . . 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 6798 . . . . . . . . . . . . . 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 2616 . . . . . . . . . 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 6771 . . . . . . . . . 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 16 . . . . . . 7  |-  ( ( x  e.  om  /\  ( z : A -1-1-onto-> x  /\  B  C_  A ) )  ->  B  e.  Fin )
3130exp32 591 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1932 . . . . 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 2623 . . 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 6    /\ wa 360   E.wex 1537    e. wcel 1621   E.wrex 2510    C_ wss 3078   class class class wbr 3920   omcom 4547   ran crn 4581    |` cres 4582   "cima 4583   -1-1->wf1 4589   -onto->wfo 4590   -1-1-onto->wf1o 4591    ~~ cen 6746   Fincfn 6749
This theorem is referenced by:  domfi  6969  diffi  6974  findcard3  6985  unfir  7010  fnfi  7019  fofinf1o  7022  fidomdm  7023  cnvfi  7025  f1fi  7028  imafi  7032  mapfi  7036  ixpfi  7037  ixpfi2  7038  mptfi  7039  elfiun  7067  marypha1lem  7070  wemapso2  7151  cantnfp1lem1  7264  oemapvali  7270  cantnflem1d  7274  cantnflem1  7275  mapfien  7283  ackbij2lem1  7729  ackbij1lem11  7740  fin23lem26  7835  fin23lem23  7836  fin23lem22  7837  fin23lem21  7849  fin11a  7893  isfin1-3  7896  axcclem  7967  pwfseqlem4  8164  hashssdif  11251  hashsslei  11255  hashbclem  11267  hashf1lem2  11271  seqcoll2  11279  isercolllem2  12016  isercoll  12018  fsumss  12075  fsum2dlem  12110  fsumcom2  12114  fsumless  12131  fsumabs  12136  fsumrlim  12146  fsumo1  12147  cvgcmpce  12153  fsumiun  12156  qshash  12162  bitsfi  12502  bitsinv1  12507  bitsinvp1  12514  sadcaddlem  12522  sadadd2lem  12524  sadadd3  12526  sadaddlem  12531  sadasslem  12535  sadeq  12537  phicl2  12710  phibnd  12713  hashdvds  12717  phiprmpw  12718  phimullem  12721  eulerthlem2  12724  eulerth  12725  sumhash  12818  prmreclem2  12838  prmreclem3  12839  prmreclem4  12840  prmreclem5  12841  1arith  12848  4sqlem11  12876  vdwlem11  12912  hashbccl  12924  ramlb  12940  0ram  12941  ramub1lem1  12947  ramub1lem2  12948  isstruct2  13031  fisuppfi  14285  lagsubg2  14513  lagsubg  14514  orbsta2  14603  odcl2  14713  oddvds2  14714  sylow1lem2  14745  sylow1lem3  14746  sylow1lem4  14747  sylow1lem5  14748  odcau  14750  pgpssslw  14760  sylow2alem2  14764  sylow2a  14765  sylow2blem1  14766  sylow2blem3  14768  slwhash  14770  fislw  14771  sylow2  14772  sylow3lem1  14773  sylow3lem3  14775  sylow3lem4  14776  sylow3lem6  14778  cyggenod  15006  gsumval3  15026  gsumzadd  15039  gsumzsplit  15041  gsumzinv  15052  gsumsub  15054  gsumunsn  15056  gsumpt  15057  gsum2d  15058  gsum2d2lem  15059  dprdfid  15087  dprdfinv  15089  dprdfadd  15090  dprdsubg  15094  dmdprdsplitlem  15107  dpjidcl  15128  ablfacrplem  15135  ablfacrp2  15137  ablfac1c  15141  ablfac1eulem  15142  ablfac1eu  15143  pgpfac1lem5  15149  pgpfaclem2  15152  pgpfaclem3  15153  ablfaclem3  15157  psrbaglecl  15947  psrbagaddcl  15948  psrbagcon  15949  psrass1lem  15955  psrbas  15956  psrlidm  15980  psrridm  15981  psrass1  15982  psrdi  15983  psrdir  15984  psrcom  15985  psrass23  15986  mvridlem  15996  mplsubg  16013  mpllss  16014  mplsubrglem  16015  mplsubrg  16016  mvrcl  16025  mplmon  16039  mplmonmul  16040  mplcoe1  16041  mplcoe3  16042  mplcoe2  16043  mplbas2  16044  psrbagsn  16068  psrbagev1  16079  evlslem2  16081  psr1baslem  16096  psropprmul  16148  coe1mul2  16178  ply1coe  16200  fctop  16573  restfpw  16742  fincmp  16952  cmpfi  16967  1stckgenlem  17080  ptbasfi  17108  ptcnplem  17147  ptcmpfi  17336  cfinfil  17420  ufinffr  17456  fin1aufil  17459  tsms0  17656  tsmsres  17658  tgptsmscls  17664  xrge0gsumle  18170  xrge0tsms  18171  fsumcn  18206  ovoliunlem1  18693  ovolicc2lem4  18711  ovolicc2lem5  18712  i1fima  18865  i1fd  18868  itg1cl  18872  itg1ge0  18873  i1f0  18874  i1f1  18877  i1fadd  18882  i1fmul  18883  itg1addlem4  18886  i1fmulc  18890  itg1mulc  18891  i1fres  18892  itg10a  18897  itg1ge0a  18898  itg1climres  18901  mbfi1fseqlem4  18905  itgfsum  19013  dvmptfsum  19154  evlslem6  19229  evlslem3  19230  tdeglem4  19278  plypf1  19426  plyexmo  19525  aannenlem2  19541  aalioulem2  19545  tayl0  19573  birthday  20081  jensenlem1  20113  jensenlem2  20114  jensen  20115  wilthlem2  20139  ppifi  20175  prmdvdsfi  20177  0sgm  20214  sgmf  20215  sgmnncl  20217  ppiprm  20221  chtprm  20223  chtdif  20228  efchtdvds  20229  ppidif  20233  ppiltx  20247  mumul  20251  sqff1o  20252  fsumdvdsdiag  20256  fsumdvdscom  20257  dvdsflsumcom  20260  musum  20263  musumsum  20264  muinv  20265  fsumdvdsmul  20267  ppiub  20275  vmasum  20287  logfac2  20288  perfectlem2  20301  dchrfi  20326  dchrabs  20331  dchrptlem1  20335  dchrptlem2  20336  dchrptlem3  20337  dchrpt  20338  lgseisenlem3  20422  lgseisenlem4  20423  lgsquadlem1  20425  lgsquadlem2  20426  lgsquadlem3  20427  chebbnd1lem1  20450  chtppilimlem1  20454  rplogsumlem2  20466  rpvmasumlem  20468  dchrvmasumlem1  20476  dchrisum0ff  20488  rpvmasum2  20493  dchrisum0re  20494  dchrisum0  20501  rplogsum  20508  dirith2  20509  vmalogdivsum2  20519  logsqvma  20523  logsqvma2  20524  selberg  20529  selberg34r  20552  pntsval2  20557  pntrlog2bndlem1  20558  deranglem  22868  subfacp1lem3  22884  subfacp1lem5  22886  subfacp1lem6  22887  erdszelem2  22894  erdszelem8  22900  erdsze2lem2  22906  vdgrf  23062  vdgrun  23064  eupath2lem3  23074  konigsberg  23082  snmlff  23083  unfinsef  24234  stfincomp  24757  finminlem  25397  finptfin  25463  finlocfin  25465  lfinpfin  25469  locfincmp  25470  nnubfi  25626  nninfnub  25627  sstotbnd2  25664  sstotbnd3  25666  cntotbnd  25686  funsnfsup  25928  lcomfsup  25934  rencldnfilem  26069  jm2.22  26254  jm2.23  26255  filnm  26358  dsmmfi  26370  dsmmacl  26373  dsmmsubg  26375  dsmmlss  26376  uvcff  26406  uvcresum  26408  frlmsplit2  26409  frlmsslsp  26414  frlmup1  26416  symgfisg  26575  symggen2  26578  psgnghm2  26604  phisum  26684
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-tr 4011  df-eprel 4198  df-id 4202  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-lim 4290  df-suc 4291  df-om 4548  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-er 6546  df-en 6750  df-fin 6753
  Copyright terms: Public domain W3C validator