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

Theorem ssfi 7079
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 )
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.

Proof of Theorem ssfi
StepHypRef Expression
1 isfi 6881 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 6867 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5445 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 5025 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5420 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3228 . . . . . . . . . . 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 7078 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 6881 . . . . . . . . . . 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 5437 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5453 . . . . . . . . . . . . . 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 2793 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 4995 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5429 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18spcev 2877 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 6867 . . . . . . . . . . . . . . 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 6909 . . . . . . . . . . . . . 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 2656 . . . . . . . . . 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 6881 . . . . . . . . . 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 590 . . . . . 6  |-  ( x  e.  om  ->  (
z : A -1-1-onto-> x  -> 
( B  C_  A  ->  B  e.  Fin )
) )
3231exlimdv 1665 . . . . 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 2663 . . 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 1529    e. wcel 1685   E.wrex 2546    C_ wss 3154   class class class wbr 4025   omcom 4656   ran crn 4690    |` cres 4691   "cima 4692   -1-1->wf1 5219   -onto->wfo 5220   -1-1-onto->wf1o 5221    ~~ cen 6856   Fincfn 6859
This theorem is referenced by:  domfi  7080  diffi  7085  findcard3  7096  unfir  7121  fnfi  7130  fofinf1o  7133  fidomdm  7134  cnvfi  7136  f1fi  7139  imafi  7144  mapfi  7148  ixpfi  7149  ixpfi2  7150  mptfi  7151  elfiun  7179  marypha1lem  7182  wemapso2  7263  cantnfp1lem1  7376  oemapvali  7382  cantnflem1d  7386  cantnflem1  7387  mapfien  7395  ackbij2lem1  7841  ackbij1lem11  7852  fin23lem26  7947  fin23lem23  7948  fin23lem22  7949  fin23lem21  7961  fin11a  8005  isfin1-3  8008  axcclem  8079  pwfseqlem4  8280  hashun3  11361  hashssdif  11369  hashsslei  11373  hashbclem  11385  hashf1lem2  11389  seqcoll2  11397  isercolllem2  12134  isercoll  12136  fsumss  12193  fsum2dlem  12228  fsumcom2  12232  fsumless  12249  fsumabs  12254  fsumrlim  12264  fsumo1  12265  cvgcmpce  12271  fsumiun  12274  qshash  12280  incexclem  12290  incexc  12291  incexc2  12292  bitsfi  12623  bitsinv1  12628  bitsinvp1  12635  sadcaddlem  12643  sadadd2lem  12645  sadadd3  12647  sadaddlem  12652  sadasslem  12656  sadeq  12658  phicl2  12831  phibnd  12834  hashdvds  12838  phiprmpw  12839  phimullem  12842  eulerthlem2  12845  eulerth  12846  sumhash  12939  prmreclem2  12959  prmreclem3  12960  prmreclem4  12961  prmreclem5  12962  1arith  12969  4sqlem11  12997  vdwlem11  13033  hashbccl  13045  ramlb  13061  0ram  13062  ramub1lem1  13068  ramub1lem2  13069  isstruct2  13152  fisuppfi  14445  lagsubg2  14673  lagsubg  14674  orbsta2  14763  odcl2  14873  oddvds2  14874  sylow1lem2  14905  sylow1lem3  14906  sylow1lem4  14907  sylow1lem5  14908  odcau  14910  pgpssslw  14920  sylow2alem2  14924  sylow2a  14925  sylow2blem1  14926  sylow2blem3  14928  slwhash  14930  fislw  14931  sylow2  14932  sylow3lem1  14933  sylow3lem3  14935  sylow3lem4  14936  sylow3lem6  14938  cyggenod  15166  gsumval3  15186  gsumzadd  15199  gsumzsplit  15201  gsumzinv  15212  gsumsub  15214  gsumunsn  15216  gsumpt  15217  gsum2d  15218  gsum2d2lem  15219  dprdfid  15247  dprdfinv  15249  dprdfadd  15250  dprdsubg  15254  dmdprdsplitlem  15267  dpjidcl  15288  ablfacrplem  15295  ablfacrp2  15297  ablfac1c  15301  ablfac1eulem  15302  ablfac1eu  15303  pgpfac1lem5  15309  pgpfaclem2  15312  pgpfaclem3  15313  ablfaclem3  15317  psrbaglecl  16110  psrbagaddcl  16111  psrbagcon  16112  psrass1lem  16118  psrbas  16119  psrlidm  16143  psrridm  16144  psrass1  16145  psrdi  16146  psrdir  16147  psrcom  16148  psrass23  16149  mvridlem  16159  mplsubg  16176  mpllss  16177  mplsubrglem  16178  mplsubrg  16179  mvrcl  16188  mplmon  16202  mplmonmul  16203  mplcoe1  16204  mplcoe3  16205  mplcoe2  16206  mplbas2  16207  psrbagsn  16231  psrbagev1  16242  evlslem2  16244  psr1baslem  16259  psropprmul  16311  coe1mul2  16341  ply1coe  16363  fctop  16736  restfpw  16905  fincmp  17115  cmpfi  17130  1stckgenlem  17243  ptbasfi  17271  ptcnplem  17310  ptcmpfi  17499  cfinfil  17583  ufinffr  17619  fin1aufil  17622  tsms0  17819  tsmsres  17821  tgptsmscls  17827  xrge0gsumle  18333  xrge0tsms  18334  fsumcn  18369  ovoliunlem1  18856  ovolicc2lem4  18874  ovolicc2lem5  18875  i1fima  19028  i1fd  19031  itg1cl  19035  itg1ge0  19036  i1f0  19037  i1f1  19040  i1fadd  19045  i1fmul  19046  itg1addlem4  19049  i1fmulc  19053  itg1mulc  19054  i1fres  19055  itg10a  19060  itg1ge0a  19061  itg1climres  19064  mbfi1fseqlem4  19068  itgfsum  19176  dvmptfsum  19317  evlslem6  19392  evlslem3  19393  tdeglem4  19441  plypf1  19589  plyexmo  19688  aannenlem2  19704  aalioulem2  19708  tayl0  19736  birthday  20244  jensenlem1  20276  jensenlem2  20277  jensen  20278  wilthlem2  20302  ppifi  20338  prmdvdsfi  20340  0sgm  20377  sgmf  20378  sgmnncl  20380  ppiprm  20384  chtprm  20386  chtdif  20391  efchtdvds  20392  ppidif  20396  ppiltx  20410  mumul  20414  sqff1o  20415  fsumdvdsdiag  20419  fsumdvdscom  20420  dvdsflsumcom  20423  musum  20426  musumsum  20427  muinv  20428  fsumdvdsmul  20430  ppiub  20438  vmasum  20450  logfac2  20451  perfectlem2  20464  dchrfi  20489  dchrabs  20494  dchrptlem1  20498  dchrptlem2  20499  dchrptlem3  20500  dchrpt  20501  lgseisenlem3  20585  lgseisenlem4  20586  lgsquadlem1  20588  lgsquadlem2  20589  lgsquadlem3  20590  chebbnd1lem1  20613  chtppilimlem1  20617  rplogsumlem2  20629  rpvmasumlem  20631  dchrvmasumlem1  20639  dchrisum0ff  20651  rpvmasum2  20656  dchrisum0re  20657  dchrisum0  20664  rplogsum  20671  dirith2  20672  vmalogdivsum2  20682  logsqvma  20686  logsqvma2  20687  selberg  20692  selberg34r  20715  pntsval2  20720  pntrlog2bndlem1  20721  infi  23022  ballotlemfelz  23043  ballotlemfp1  23044  ballotlemfc0  23045  ballotlemfcc  23046  ballotlemiex  23054  ballotlemsup  23057  ballotlemfg  23078  ballotlemfrc  23079  ballotlemfrceq  23081  ballotth  23090  deranglem  23102  subfacp1lem3  23118  subfacp1lem5  23120  subfacp1lem6  23121  erdszelem2  23128  erdszelem8  23134  erdsze2lem2  23140  vdgrf  23296  vdgrun  23298  eupath2lem3  23308  konigsberg  23316  snmlff  23317  unfinsef  24468  stfincomp  24991  finminlem  25631  finptfin  25697  finlocfin  25699  lfinpfin  25703  locfincmp  25704  nnubfi  25860  nninfnub  25861  sstotbnd2  25898  sstotbnd3  25900  cntotbnd  25920  funsnfsup  26162  lcomfsup  26168  rencldnfilem  26303  jm2.22  26488  jm2.23  26489  filnm  26592  dsmmfi  26604  dsmmacl  26607  dsmmsubg  26609  dsmmlss  26610  uvcff  26640  uvcresum  26642  frlmsplit2  26643  frlmsslsp  26648  frlmup1  26650  symgfisg  26809  symggen2  26812  psgnghm2  26838  phisum  26918
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-er 6656  df-en 6860  df-fin 6863
  Copyright terms: Public domain W3C validator