Theorem ssfi 7817

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 7618	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7603	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5843	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5197	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5818	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3491	. . . . . . . . . . 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 7816	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7618	. . . . . . . . . . 11 |- ( ( z " B ) e. Fin <-> E. y e. om ( z " B ) ~~ y )
10	8, 9	sylib 201	. . . . . . . . . 10 |- ( ( x e. om /\ ( z " B ) C_ x ) -> E. y e. om ( z " B ) ~~ y )
11	7, 10	sylan2 481	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 728	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5835	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5850	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 478	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 3059	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5166	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5827	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3152	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7603	. . . . . . . . . . . . . . 15 |- ( B ~~ ( z " B ) <-> E. x x : B -1-1-onto-> ( z " B ) )
21	19, 20	sylibr 217	. . . . . . . . . . . . . 14 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> B ~~ ( z " B ) )
22		entr 7646	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 478	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 478	. . . . . . . . . . . 12 |- ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25	24	ex 440	. . . . . . . . . . 11 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26	25	reximdv 2872	. . . . . . . . . 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 7618	. . . . . . . . . 10 |- ( B e. Fin <-> E. y e. om B ~~ y )
28	26, 27	syl6ibr 235	. . . . . . . . 9 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. om ( z " B ) ~~ y -> B e. Fin ) )
29	28	adantl 472	. . . . . . . 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 614	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1789	. . . . 5 |- ( x e. om -> ( E. z z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
33	2, 32	syl5bi 225	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C_ A -> B e. Fin ) ) )
34	33	rexlimiv 2884	. . 3 |- ( E. x e. om A ~~ x -> ( B C_ A -> B e. Fin ) )
35	1, 34	sylbi 200	. 2 |- ( A e. Fin -> ( B C_ A -> B e. Fin ) )
36	35	imp 435	1 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   /\ wa 375   E.wex 1673   e. wcel 1897   E.wrex 2749   C_ wss 3415   class class class wbr 4415   ran crn 4853   |` cres 4854   "cima 4855   -1-1->wf1 5597   -onto->wfo 5598   -1-1-onto->wf1o 5599   omcom 6718   ~~ cen 7591   Fincfn 7594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-om 6719  df-er 7388  df-en 7595  df-fin 7598

This theorem is referenced by:  domfi  7818  infi  7820  finresfin  7822  diffi  7828  findcard3  7839  unfir  7864  fnfi  7874  fofinf1o  7877  cnvfi  7881  f1fi  7886  imafi  7892  mapfi  7895  ixpfi  7896  ixpfi2  7897  mptfi  7898  cnvimamptfin  7900  fisuppfi  7916  suppssfifsupp  7923  fsuppunbi  7929  snopfsupp  7931  fsuppres  7933  ressuppfi  7934  fsuppmptif  7938  fsuppco2  7941  fsuppcor  7942  sniffsupp  7948  elfiun  7969  marypha1lem  7972  wemapso2lem  8092  cantnfp1lem1  8208  oemapvali  8214  ackbij2lem1  8674  ackbij1lem11  8685  fin23lem26  8780  fin23lem23  8781  fin23lem21  8794  fin11a  8838  isfin1-3  8841  axcclem  8912  pwfseqlem4  9112  ssnn0fi  12228  hashun3  12594  hashss  12617  hashssdif  12620  hashsslei  12630  hashbclem  12647  hashf1lem2  12651  seqcoll2  12660  pr2pwpr  12668  isercolllem2  13777  isercoll  13779  fsum2dlem  13879  fsumcom2  13883  fsumless  13904  fsumabs  13909  fsumrlim  13919  fsumo1  13920  cvgcmpce  13926  fsumiun  13929  qshash  13933  incexclem  13942  incexc  13943  incexc2  13944  fprod2dlem  14082  fprodcom2  14086  bitsfi  14459  bitsinv1  14464  bitsinvp1  14471  sadcaddlem  14479  sadadd2lem  14481  sadadd3  14483  sadaddlem  14488  sadasslem  14492  sadeq  14494  phicl2  14764  phibnd  14767  hashdvds  14771  phiprmpw  14772  phimullem  14775  eulerthlem2  14778  eulerth  14779  sumhash  14889  prmreclem2  14909  prmreclem3  14910  prmreclem4  14911  prmreclem5  14912  1arith  14919  4sqlem11  14947  vdwlem11  14989  hashbccl  15003  ramlb  15025  0ram  15026  ramub1lem1  15032  ramub1lem2  15033  prmgaplem3  15071  prmgaplem4  15072  isstruct2  15178  lagsubg2  16926  lagsubg  16927  orbsta2  17016  symgbasfi  17075  symgfisg  17157  symggen2  17160  odcl2  17264  oddvds2  17265  sylow1lem2  17299  sylow1lem3  17300  sylow1lem4  17301  sylow1lem5  17302  odcau  17304  pgpssslw  17314  sylow2alem2  17318  sylow2a  17319  sylow2blem1  17320  sylow2blem3  17322  slwhash  17324  fislw  17325  sylow2  17326  sylow3lem1  17327  sylow3lem3  17329  sylow3lem4  17330  sylow3lem6  17332  cyggenod  17567  gsumval3lem1  17587  gsumval3lem2  17588  gsumval3  17589  gsumzadd  17603  gsumpt  17642  gsum2dlem1  17650  gsum2dlem2  17651  gsum2d  17652  gsum2d2lem  17653  dprdfadd  17701  ablfacrplem  17746  ablfacrp2  17748  ablfac1c  17752  ablfac1eulem  17753  ablfac1eu  17754  pgpfac1lem5  17760  pgpfaclem2  17763  pgpfaclem3  17764  ablfaclem3  17768  lcomfsupp  18176  psrbaglecl  18641  psrbagaddcl  18642  psrbagcon  18643  mplsubg  18709  mpllss  18710  mplcoe5  18740  psrbagsn  18766  psr1baslem  18826  dsmmfi  19349  dsmmacl  19352  dsmmsubg  19354  dsmmlss  19355  frlmsslsp  19402  mamures  19463  submabas  19651  mdetdiaglem  19671  mdetrlin  19675  mdetrsca  19676  mdetralt  19681  maducoeval2  19713  madugsum  19716  fctop  20067  restfpw  20243  fincmp  20456  cmpfi  20471  bwth  20473  finlocfin  20583  lfinpfin  20587  locfincmp  20589  1stckgenlem  20616  ptbasfi  20644  ptcnplem  20684  ptcmpfi  20876  cfinfil  20956  ufinffr  20992  fin1aufil  20995  tsmsres  21206  xrge0gsumle  21899  xrge0tsms  21900  fsumcn  21950  rrxcph  22399  rrxmval  22407  ovoliunlem1  22503  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  ovolicc2lem5  22523  i1fima  22684  i1fd  22687  itg1cl  22691  itg1ge0  22692  i1f0  22693  i1f1  22696  i1fadd  22701  i1fmul  22702  itg1addlem4  22705  i1fmulc  22709  itg1mulc  22710  i1fres  22711  itg10a  22716  itg1ge0a  22717  itg1climres  22720  mbfi1fseqlem4  22724  itgfsum  22832  dvmptfsum  22975  plyexmo  23314  aannenlem2  23333  aalioulem2  23337  birthday  23928  jensenlem1  23960  jensenlem2  23961  jensen  23962  wilthlem2  24042  ppifi  24080  prmdvdsfi  24082  0sgm  24119  sgmf  24120  sgmnncl  24122  ppiprm  24126  chtprm  24128  chtdif  24133  efchtdvds  24134  ppidif  24138  ppiltx  24152  mumul  24156  sqff1o  24157  fsumdvdsdiag  24161  fsumdvdscom  24162  dvdsflsumcom  24165  musum  24168  musumsum  24169  muinv  24170  fsumdvdsmul  24172  ppiub  24180  vmasum  24192  logfac2  24193  perfectlem2  24206  dchrfi  24231  dchrabs  24236  dchrptlem1  24240  dchrptlem2  24241  dchrpt  24243  lgsquadlem1  24330  lgsquadlem2  24331  lgsquadlem3  24332  chebbnd1lem1  24355  chtppilimlem1  24359  rplogsumlem2  24371  rpvmasumlem  24373  dchrvmasumlem1  24381  dchrisum0ff  24393  rpvmasum2  24398  dchrisum0re  24399  dchrisum0  24406  rplogsum  24413  dirith2  24414  vmalogdivsum2  24424  logsqvma  24428  logsqvma2  24429  selberg  24434  selberg34r  24457  pntsval2  24462  pntrlog2bndlem1  24463  cusgrafi  25258  wwlknfi  25514  hashwwlkext  25522  clwwlknfi  25554  qerclwwlknfi  25605  vdgrfiun  25678  eupath2lem3  25755  konigsberg  25763  relfi  28261  imafi2  28340  unifi3  28341  ffsrn  28362  gsumle  28590  xrge0tsmsd  28596  hasheuni  28954  carsgclctunlem1  29197  sibfof  29221  sitgclg  29223  oddpwdc  29235  eulerpartlems  29241  eulerpartlemb  29249  eulerpartlemmf  29256  eulerpartlemgf  29260  eulerpartlemgs2  29261  coinfliplem  29359  coinflippv  29364  ballotlemfelz  29371  ballotlemfp1  29372  ballotlemfc0  29373  ballotlemfcc  29374  ballotlemiex  29382  ballotlemsup  29385  ballotlemfg  29406  ballotlemfrc  29407  ballotlemfrceq  29409  ballotth  29418  ballotlemiexOLD  29420  ballotlemsupOLD  29423  ballotlemfgOLD  29444  ballotlemfrcOLD  29445  ballotlemfrceqOLD  29447  ballotthOLD  29456  deranglem  29937  subfacp1lem3  29953  subfacp1lem5  29955  subfacp1lem6  29956  erdszelem2  29963  erdszelem8  29969  erdsze2lem2  29975  snmlff  30100  mvrsfpw  30192  finminlem  31022  topdifinffinlem  31794  poimirlem9  31993  poimirlem26  32010  poimirlem27  32011  poimirlem28  32012  poimirlem30  32014  poimirlem32  32016  itg2addnclem2  32038  nnubfi  32123  nninfnub  32124  sstotbnd2  32150  cntotbnd  32172  rencldnfilem  35707  jm2.22  35894  jm2.23  35895  filnm  35992  phisum  36120  pwssfi  37418  ssfid  37451  disjinfi  37505  fsumiunss  37691  fprodexp  37711  fprodabs2  37712  mccllem  37714  sumnnodd  37747  fprodcncf  37816  dvmptfprod  37857  dvnprodlem1  37858  dvnprodlem2  37859  fourierdlem25  38031  fourierdlem37  38044  fourierdlem51  38058  fourierdlem79  38086  fouriersw  38132  etransclem16  38152  etransclem24  38160  etransclem33  38169  etransclem44  38180  sge0resplit  38285  sge0iunmptlemfi  38292  sge0iunmptlemre  38294  carageniuncllem2  38380  hsphoidmvle2  38444  hsphoidmvle  38445  hoidmvlelem4  38457  hoidmvlelem5  38458  perfectALTVlem2  38881  cusgrfi  39568  rmsuppfi  40430  mndpsuppfi  40432  scmsuppfi  40434  suppmptcfin  40436