Theorem ssfi 7740

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.

Step	Hyp	Ref	Expression
1		isfi 7542	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7528	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5776	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5136	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5751	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3450	. . . . . . . . . . 11 |- ( z : A -onto-> x -> ( z " B ) C_ x )
7	3, 6	syl 17	. . . . . . . . . 10 |- ( z : A -1-1-onto-> x -> ( z " B ) C_ x )
8		ssnnfi 7739	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7542	. . . . . . . . . . 11 |- ( ( z " B ) e. Fin <-> E. y e. om ( z " B ) ~~ y )
10	8, 9	sylib 199	. . . . . . . . . 10 |- ( ( x e. om /\ ( z " B ) C_ x ) -> E. y e. om ( z " B ) ~~ y )
11	7, 10	sylan2 476	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 721	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5768	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5783	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 473	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 3020	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5105	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5760	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3111	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7528	. . . . . . . . . . . . . . 15 |- ( B ~~ ( z " B ) <-> E. x x : B -1-1-onto-> ( z " B ) )
21	19, 20	sylibr 215	. . . . . . . . . . . . . 14 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> B ~~ ( z " B ) )
22		entr 7570	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 473	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 473	. . . . . . . . . . . 12 |- ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25	24	ex 435	. . . . . . . . . . 11 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26	25	reximdv 2833	. . . . . . . . . 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 7542	. . . . . . . . . 10 |- ( B e. Fin <-> E. y e. om B ~~ y )
28	26, 27	syl6ibr 230	. . . . . . . . 9 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. om ( z " B ) ~~ y -> B e. Fin ) )
29	28	adantl 467	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> ( E. y e. om ( z " B ) ~~ y -> B e. Fin ) )
30	12, 29	mpd 15	. . . . . . 7 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> B e. Fin )
31	30	exp32 608	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1772	. . . . 5 |- ( x e. om -> ( E. z z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
33	2, 32	syl5bi 220	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C_ A -> B e. Fin ) ) )
34	33	rexlimiv 2845	. . 3 |- ( E. x e. om A ~~ x -> ( B C_ A -> B e. Fin ) )
35	1, 34	sylbi 198	. 2 |- ( A e. Fin -> ( B C_ A -> B e. Fin ) )
36	35	imp 430	1 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   /\ wa 370   E.wex 1657   e. wcel 1872   E.wrex 2710   C_ wss 3374   class class class wbr 4361   ran crn 4792   |` cres 4793   "cima 4794   -1-1->wf1 5536   -onto->wfo 5537   -1-1-onto->wf1o 5538   omcom 6645   ~~ cen 7516   Fincfn 7519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-om 6646  df-er 7313  df-en 7520  df-fin 7523

This theorem is referenced by:  domfi  7741  infi  7743  finresfin  7745  diffi  7751  findcard3  7762  unfir  7787  fnfi  7797  fofinf1o  7800  cnvfi  7804  f1fi  7809  imafi  7815  mapfi  7818  ixpfi  7819  ixpfi2  7820  mptfi  7821  cnvimamptfin  7823  fisuppfi  7839  suppssfifsupp  7846  fsuppunbi  7852  snopfsupp  7854  fsuppres  7856  ressuppfi  7857  fsuppmptif  7861  fsuppco2  7864  fsuppcor  7865  sniffsupp  7871  elfiun  7892  marypha1lem  7895  wemapso2lem  8015  cantnfp1lem1  8130  oemapvali  8136  ackbij2lem1  8595  ackbij1lem11  8606  fin23lem26  8701  fin23lem23  8702  fin23lem21  8715  fin11a  8759  isfin1-3  8762  axcclem  8833  pwfseqlem4  9033  ssnn0fi  12142  hashun3  12508  hashss  12531  hashssdif  12532  hashsslei  12541  hashbclem  12558  hashf1lem2  12562  seqcoll2  12571  pr2pwpr  12579  isercolllem2  13667  isercoll  13669  fsum2dlem  13769  fsumcom2  13773  fsumless  13794  fsumabs  13799  fsumrlim  13809  fsumo1  13810  cvgcmpce  13816  fsumiun  13819  qshash  13823  incexclem  13832  incexc  13833  incexc2  13834  fprod2dlem  13972  fprodcom2  13976  bitsfi  14349  bitsinv1  14354  bitsinvp1  14361  sadcaddlem  14369  sadadd2lem  14371  sadadd3  14373  sadaddlem  14378  sadasslem  14382  sadeq  14384  phicl2  14654  phibnd  14657  hashdvds  14661  phiprmpw  14662  phimullem  14665  eulerthlem2  14668  eulerth  14669  sumhash  14779  prmreclem2  14799  prmreclem3  14800  prmreclem4  14801  prmreclem5  14802  1arith  14809  4sqlem11  14837  vdwlem11  14879  hashbccl  14893  ramlb  14915  0ram  14916  ramub1lem1  14922  ramub1lem2  14923  prmgaplem3  14961  prmgaplem4  14962  isstruct2  15068  lagsubg2  16816  lagsubg  16817  orbsta2  16906  symgbasfi  16965  symgfisg  17047  symggen2  17050  odcl2  17154  oddvds2  17155  sylow1lem2  17189  sylow1lem3  17190  sylow1lem4  17191  sylow1lem5  17192  odcau  17194  pgpssslw  17204  sylow2alem2  17208  sylow2a  17209  sylow2blem1  17210  sylow2blem3  17212  slwhash  17214  fislw  17215  sylow2  17216  sylow3lem1  17217  sylow3lem3  17219  sylow3lem4  17220  sylow3lem6  17222  cyggenod  17457  gsumval3lem1  17477  gsumval3lem2  17478  gsumval3  17479  gsumzadd  17493  gsumpt  17532  gsum2dlem1  17540  gsum2dlem2  17541  gsum2d  17542  gsum2d2lem  17543  dprdfadd  17591  ablfacrplem  17636  ablfacrp2  17638  ablfac1c  17642  ablfac1eulem  17643  ablfac1eu  17644  pgpfac1lem5  17650  pgpfaclem2  17653  pgpfaclem3  17654  ablfaclem3  17658  lcomfsupp  18066  psrbaglecl  18531  psrbagaddcl  18532  psrbagcon  18533  mplsubg  18599  mpllss  18600  mplcoe5  18630  psrbagsn  18656  psr1baslem  18716  dsmmfi  19238  dsmmacl  19241  dsmmsubg  19243  dsmmlss  19244  frlmsslsp  19291  mamures  19352  submabas  19540  mdetdiaglem  19560  mdetrlin  19564  mdetrsca  19565  mdetralt  19570  maducoeval2  19602  madugsum  19605  fctop  19956  restfpw  20132  fincmp  20345  cmpfi  20360  bwth  20362  finlocfin  20472  lfinpfin  20476  locfincmp  20478  1stckgenlem  20505  ptbasfi  20533  ptcnplem  20573  ptcmpfi  20765  cfinfil  20845  ufinffr  20881  fin1aufil  20884  tsmsres  21095  xrge0gsumle  21788  xrge0tsms  21789  fsumcn  21839  rrxcph  22288  rrxmval  22296  ovoliunlem1  22392  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ovolicc2lem5  22412  i1fima  22573  i1fd  22576  itg1cl  22580  itg1ge0  22581  i1f0  22582  i1f1  22585  i1fadd  22590  i1fmul  22591  itg1addlem4  22594  i1fmulc  22598  itg1mulc  22599  i1fres  22600  itg10a  22605  itg1ge0a  22606  itg1climres  22609  mbfi1fseqlem4  22613  itgfsum  22721  dvmptfsum  22864  plyexmo  23203  aannenlem2  23222  aalioulem2  23226  birthday  23817  jensenlem1  23849  jensenlem2  23850  jensen  23851  wilthlem2  23931  ppifi  23969  prmdvdsfi  23971  0sgm  24008  sgmf  24009  sgmnncl  24011  ppiprm  24015  chtprm  24017  chtdif  24022  efchtdvds  24023  ppidif  24027  ppiltx  24041  mumul  24045  sqff1o  24046  fsumdvdsdiag  24050  fsumdvdscom  24051  dvdsflsumcom  24054  musum  24057  musumsum  24058  muinv  24059  fsumdvdsmul  24061  ppiub  24069  vmasum  24081  logfac2  24082  perfectlem2  24095  dchrfi  24120  dchrabs  24125  dchrptlem1  24129  dchrptlem2  24130  dchrpt  24132  lgsquadlem1  24219  lgsquadlem2  24220  lgsquadlem3  24221  chebbnd1lem1  24244  chtppilimlem1  24248  rplogsumlem2  24260  rpvmasumlem  24262  dchrvmasumlem1  24270  dchrisum0ff  24282  rpvmasum2  24287  dchrisum0re  24288  dchrisum0  24295  rplogsum  24302  dirith2  24303  vmalogdivsum2  24313  logsqvma  24317  logsqvma2  24318  selberg  24323  selberg34r  24346  pntsval2  24351  pntrlog2bndlem1  24352  cusgrafi  25147  wwlknfi  25403  hashwwlkext  25411  clwwlknfi  25443  qerclwwlknfi  25494  vdgrfiun  25567  eupath2lem3  25644  konigsberg  25652  relfi  28154  imafi2  28233  unifi3  28234  ffsrn  28259  gsumle  28488  xrge0tsmsd  28495  hasheuni  28853  carsgclctunlem1  29096  sibfof  29120  sitgclg  29122  oddpwdc  29134  eulerpartlems  29140  eulerpartlemb  29148  eulerpartlemmf  29155  eulerpartlemgf  29159  eulerpartlemgs2  29160  coinfliplem  29258  coinflippv  29263  ballotlemfelz  29270  ballotlemfp1  29271  ballotlemfc0  29272  ballotlemfcc  29273  ballotlemiex  29281  ballotlemsup  29284  ballotlemfg  29305  ballotlemfrc  29306  ballotlemfrceq  29308  ballotth  29317  ballotlemiexOLD  29319  ballotlemsupOLD  29322  ballotlemfgOLD  29343  ballotlemfrcOLD  29344  ballotlemfrceqOLD  29346  ballotthOLD  29355  deranglem  29836  subfacp1lem3  29852  subfacp1lem5  29854  subfacp1lem6  29855  erdszelem2  29862  erdszelem8  29868  erdsze2lem2  29874  snmlff  29999  mvrsfpw  30091  finminlem  30918  topdifinffinlem  31657  poimirlem9  31856  poimirlem26  31873  poimirlem27  31874  poimirlem28  31875  poimirlem30  31877  poimirlem32  31879  itg2addnclem2  31901  nnubfi  31986  nninfnub  31987  sstotbnd2  32013  cntotbnd  32035  rencldnfilem  35575  jm2.22  35763  jm2.23  35764  filnm  35861  phisum  35989  pwssfi  37297  ssfid  37331  disjinfi  37372  fsumiunss  37538  fprodexp  37557  fprodabs2  37558  mccllem  37560  sumnnodd  37593  fprodcncf  37662  dvmptfprod  37703  dvnprodlem1  37704  dvnprodlem2  37705  fourierdlem25  37877  fourierdlem37  37890  fourierdlem51  37904  fourierdlem79  37932  fouriersw  37978  etransclem16  37998  etransclem24  38006  etransclem33  38015  etransclem44  38026  sge0resplit  38099  sge0iunmptlemfi  38106  sge0iunmptlemre  38108  carageniuncllem2  38194  hsphoidmvle2  38254  hsphoidmvle  38255  hoidmvlelem4  38267  hoidmvlelem5  38268  perfectALTVlem2  38657  cusgrfi  39247  rmsuppfi  39751  mndpsuppfi  39753  scmsuppfi  39755  suppmptcfin  39757