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

Theorem ssfi 7037
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 6839 . . 3  |-  ( A  e.  Fin  <->  E. x  e.  om  A  ~~  x
)
2 bren 6825 . . . . 5  |-  ( A 
~~  x  <->  E. z 
z : A -1-1-onto-> x )
3 f1ofo 5403 . . . . . . . . . . 11  |-  ( z : A -1-1-onto-> x  ->  z : A -onto-> x )
4 imassrn 4999 . . . . . . . . . . . 12  |-  ( z
" B )  C_  ran  z
5 forn 5378 . . . . . . . . . . . 12  |-  ( z : A -onto-> x  ->  ran  z  =  x
)
64, 5syl5sseq 3187 . . . . . . . . . . 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 7036 . . . . . . . . . . 11  |-  ( ( x  e.  om  /\  ( z " B
)  C_  x )  ->  ( z " B
)  e.  Fin )
9 isfi 6839 . . . . . . . . . . 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 5395 . . . . . . . . . . . . . 14  |-  ( z : A -1-1-onto-> x  ->  z : A -1-1-> x )
14 f1ores 5411 . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
1716resex 4969 . . . . . . . . . . . . . . . 16  |-  ( z  |`  B )  e.  _V
18 f1oeq1 5387 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( z  |`  B )  ->  (
x : B -1-1-onto-> ( z
" B )  <->  ( z  |`  B ) : B -1-1-onto-> (
z " B ) ) )
1917, 18cla4ev 2843 . . . . . . . . . . . . . . 15  |-  ( ( z  |`  B ) : B -1-1-onto-> ( z " B
)  ->  E. x  x : B -1-1-onto-> ( z " B
) )
20 bren 6825 . . . . . . . . . . . . . . 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 6867 . . . . . . . . . . . . . 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 2627 . . . . . . . . . 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 6839 . . . . . . . . . 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 1933 . . . . 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 2634 . . 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 2517    C_ wss 3113   class class class wbr 3983   omcom 4614   ran crn 4648    |` cres 4649   "cima 4650   -1-1->wf1 4656   -onto->wfo 4657   -1-1-onto->wf1o 4658    ~~ cen 6814   Fincfn 6817
This theorem is referenced by:  domfi  7038  diffi  7043  findcard3  7054  unfir  7079  fnfi  7088  fofinf1o  7091  fidomdm  7092  cnvfi  7094  f1fi  7097  imafi  7102  mapfi  7106  ixpfi  7107  ixpfi2  7108  mptfi  7109  elfiun  7137  marypha1lem  7140  wemapso2  7221  cantnfp1lem1  7334  oemapvali  7340  cantnflem1d  7344  cantnflem1  7345  mapfien  7353  ackbij2lem1  7799  ackbij1lem11  7810  fin23lem26  7905  fin23lem23  7906  fin23lem22  7907  fin23lem21  7919  fin11a  7963  isfin1-3  7966  axcclem  8037  pwfseqlem4  8238  hashssdif  11325  hashsslei  11329  hashbclem  11341  hashf1lem2  11345  seqcoll2  11353  isercolllem2  12090  isercoll  12092  fsumss  12149  fsum2dlem  12184  fsumcom2  12188  fsumless  12205  fsumabs  12210  fsumrlim  12220  fsumo1  12221  cvgcmpce  12227  fsumiun  12230  qshash  12236  bitsfi  12576  bitsinv1  12581  bitsinvp1  12588  sadcaddlem  12596  sadadd2lem  12598  sadadd3  12600  sadaddlem  12605  sadasslem  12609  sadeq  12611  phicl2  12784  phibnd  12787  hashdvds  12791  phiprmpw  12792  phimullem  12795  eulerthlem2  12798  eulerth  12799  sumhash  12892  prmreclem2  12912  prmreclem3  12913  prmreclem4  12914  prmreclem5  12915  1arith  12922  4sqlem11  12950  vdwlem11  12986  hashbccl  12998  ramlb  13014  0ram  13015  ramub1lem1  13021  ramub1lem2  13022  isstruct2  13105  fisuppfi  14398  lagsubg2  14626  lagsubg  14627  orbsta2  14716  odcl2  14826  oddvds2  14827  sylow1lem2  14858  sylow1lem3  14859  sylow1lem4  14860  sylow1lem5  14861  odcau  14863  pgpssslw  14873  sylow2alem2  14877  sylow2a  14878  sylow2blem1  14879  sylow2blem3  14881  slwhash  14883  fislw  14884  sylow2  14885  sylow3lem1  14886  sylow3lem3  14888  sylow3lem4  14889  sylow3lem6  14891  cyggenod  15119  gsumval3  15139  gsumzadd  15152  gsumzsplit  15154  gsumzinv  15165  gsumsub  15167  gsumunsn  15169  gsumpt  15170  gsum2d  15171  gsum2d2lem  15172  dprdfid  15200  dprdfinv  15202  dprdfadd  15203  dprdsubg  15207  dmdprdsplitlem  15220  dpjidcl  15241  ablfacrplem  15248  ablfacrp2  15250  ablfac1c  15254  ablfac1eulem  15255  ablfac1eu  15256  pgpfac1lem5  15262  pgpfaclem2  15265  pgpfaclem3  15266  ablfaclem3  15270  psrbaglecl  16063  psrbagaddcl  16064  psrbagcon  16065  psrass1lem  16071  psrbas  16072  psrlidm  16096  psrridm  16097  psrass1  16098  psrdi  16099  psrdir  16100  psrcom  16101  psrass23  16102  mvridlem  16112  mplsubg  16129  mpllss  16130  mplsubrglem  16131  mplsubrg  16132  mvrcl  16141  mplmon  16155  mplmonmul  16156  mplcoe1  16157  mplcoe3  16158  mplcoe2  16159  mplbas2  16160  psrbagsn  16184  psrbagev1  16195  evlslem2  16197  psr1baslem  16212  psropprmul  16264  coe1mul2  16294  ply1coe  16316  fctop  16689  restfpw  16858  fincmp  17068  cmpfi  17083  1stckgenlem  17196  ptbasfi  17224  ptcnplem  17263  ptcmpfi  17452  cfinfil  17536  ufinffr  17572  fin1aufil  17575  tsms0  17772  tsmsres  17774  tgptsmscls  17780  xrge0gsumle  18286  xrge0tsms  18287  fsumcn  18322  ovoliunlem1  18809  ovolicc2lem4  18827  ovolicc2lem5  18828  i1fima  18981  i1fd  18984  itg1cl  18988  itg1ge0  18989  i1f0  18990  i1f1  18993  i1fadd  18998  i1fmul  18999  itg1addlem4  19002  i1fmulc  19006  itg1mulc  19007  i1fres  19008  itg10a  19013  itg1ge0a  19014  itg1climres  19017  mbfi1fseqlem4  19021  itgfsum  19129  dvmptfsum  19270  evlslem6  19345  evlslem3  19346  tdeglem4  19394  plypf1  19542  plyexmo  19641  aannenlem2  19657  aalioulem2  19661  tayl0  19689  birthday  20197  jensenlem1  20229  jensenlem2  20230  jensen  20231  wilthlem2  20255  ppifi  20291  prmdvdsfi  20293  0sgm  20330  sgmf  20331  sgmnncl  20333  ppiprm  20337  chtprm  20339  chtdif  20344  efchtdvds  20345  ppidif  20349  ppiltx  20363  mumul  20367  sqff1o  20368  fsumdvdsdiag  20372  fsumdvdscom  20373  dvdsflsumcom  20376  musum  20379  musumsum  20380  muinv  20381  fsumdvdsmul  20383  ppiub  20391  vmasum  20403  logfac2  20404  perfectlem2  20417  dchrfi  20442  dchrabs  20447  dchrptlem1  20451  dchrptlem2  20452  dchrptlem3  20453  dchrpt  20454  lgseisenlem3  20538  lgseisenlem4  20539  lgsquadlem1  20541  lgsquadlem2  20542  lgsquadlem3  20543  chebbnd1lem1  20566  chtppilimlem1  20570  rplogsumlem2  20582  rpvmasumlem  20584  dchrvmasumlem1  20592  dchrisum0ff  20604  rpvmasum2  20609  dchrisum0re  20610  dchrisum0  20617  rplogsum  20624  dirith2  20625  vmalogdivsum2  20635  logsqvma  20639  logsqvma2  20640  selberg  20645  selberg34r  20668  pntsval2  20673  pntrlog2bndlem1  20674  infi  22975  ballotlemfelz  22996  ballotlemfp1  22997  ballotlemfc0  22998  ballotlemfcc  22999  ballotlemiex  23007  ballotlemsup  23010  ballotlemfg  23031  ballotlemfrc  23032  ballotlemfrceq  23034  ballotth  23043  deranglem  23055  subfacp1lem3  23071  subfacp1lem5  23073  subfacp1lem6  23074  erdszelem2  23081  erdszelem8  23087  erdsze2lem2  23093  vdgrf  23249  vdgrun  23251  eupath2lem3  23261  konigsberg  23269  snmlff  23270  unfinsef  24421  stfincomp  24944  finminlem  25584  finptfin  25650  finlocfin  25652  lfinpfin  25656  locfincmp  25657  nnubfi  25813  nninfnub  25814  sstotbnd2  25851  sstotbnd3  25853  cntotbnd  25873  funsnfsup  26115  lcomfsup  26121  rencldnfilem  26256  jm2.22  26441  jm2.23  26442  filnm  26545  dsmmfi  26557  dsmmacl  26560  dsmmsubg  26562  dsmmlss  26563  uvcff  26593  uvcresum  26595  frlmsplit2  26596  frlmsslsp  26601  frlmup1  26603  symgfisg  26762  symggen2  26765  psgnghm2  26791  phisum  26871
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 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470
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 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-er 6614  df-en 6818  df-fin 6821
  Copyright terms: Public domain W3C validator