Theorem ssfi 7525

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 7325	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7311	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5643	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5175	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5618	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3399	. . . . . . . . . . 11 |- ( z : A -onto-> x -> ( z " B ) C_ x )
7	3, 6	syl 16	. . . . . . . . . 10 |- ( z : A -1-1-onto-> x -> ( z " B ) C_ x )
8		ssnnfi 7524	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7325	. . . . . . . . . . 11 |- ( ( z " B ) e. Fin <-> E. y e. om ( z " B ) ~~ y )
10	8, 9	sylib 196	. . . . . . . . . 10 |- ( ( x e. om /\ ( z " B ) C_ x ) -> E. y e. om ( z " B ) ~~ y )
11	7, 10	sylan2 474	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 716	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5635	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5650	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 471	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 2970	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5145	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5627	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3059	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7311	. . . . . . . . . . . . . . 15 |- ( B ~~ ( z " B ) <-> E. x x : B -1-1-onto-> ( z " B ) )
21	19, 20	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> B ~~ ( z " B ) )
22		entr 7353	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 471	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 471	. . . . . . . . . . . 12 |- ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25	24	ex 434	. . . . . . . . . . 11 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26	25	reximdv 2822	. . . . . . . . . 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 7325	. . . . . . . . . 10 |- ( B e. Fin <-> E. y e. om B ~~ y )
28	26, 27	syl6ibr 227	. . . . . . . . 9 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. om ( z " B ) ~~ y -> B e. Fin ) )
29	28	adantl 466	. . . . . . . 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 605	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1690	. . . . 5 |- ( x e. om -> ( E. z z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
33	2, 32	syl5bi 217	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C_ A -> B e. Fin ) ) )
34	33	rexlimiv 2830	. . 3 |- ( E. x e. om A ~~ x -> ( B C_ A -> B e. Fin ) )
35	1, 34	sylbi 195	. 2 |- ( A e. Fin -> ( B C_ A -> B e. Fin ) )
36	35	imp 429	1 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   /\ wa 369   E.wex 1586   e. wcel 1756   E.wrex 2711   C_ wss 3323   class class class wbr 4287   ran crn 4836   |` cres 4837   "cima 4838   -1-1->wf1 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412   omcom 6471   ~~ cen 7299   Fincfn 7302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-om 6472  df-er 7093  df-en 7303  df-fin 7306

This theorem is referenced by:  domfi  7526  infi  7528  finresfin  7530  diffi  7535  findcard3  7547  unfir  7572  fnfi  7581  fofinf1o  7584  cnvfi  7587  f1fi  7590  imafi  7596  mapfi  7599  ixpfi  7600  ixpfi2  7601  mptfi  7602  cnvimamptfin  7604  fisuppfi  7620  suppssfifsupp  7627  fsuppunbi  7633  snopfsupp  7635  fsuppres  7637  ressuppfi  7638  fsuppmptif  7641  fsuppco2  7644  fsuppcor  7645  sniffsupp  7651  elfiun  7672  marypha1lem  7675  wemapso2OLD  7758  wemapso2lem  7759  cantnfp1lem1  7878  oemapvali  7884  cantnfp1lem1OLD  7904  cantnflem1dOLD  7911  cantnflem1OLD  7912  mapfienOLD  7919  ackbij2lem1  8380  ackbij1lem11  8391  fin23lem26  8486  fin23lem23  8487  fin23lem21  8500  fin11a  8544  isfin1-3  8547  axcclem  8618  pwfseqlem4  8821  hashun3  12139  hashss  12158  hashssdif  12159  hashsslei  12168  pr2pwpr  12175  hashbclem  12197  hashf1lem2  12201  seqcoll2  12209  isercolllem2  13135  isercoll  13137  fsumss  13194  fsum2dlem  13229  fsumcom2  13233  fsumless  13251  fsumabs  13256  fsumrlim  13266  fsumo1  13267  cvgcmpce  13273  fsumiun  13276  qshash  13282  incexclem  13291  incexc  13292  incexc2  13293  bitsfi  13625  bitsinv1  13630  bitsinvp1  13637  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  phicl2  13835  phibnd  13838  hashdvds  13842  phiprmpw  13843  phimullem  13846  eulerthlem2  13849  eulerth  13850  sumhash  13950  prmreclem2  13970  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  1arith  13980  4sqlem11  14008  vdwlem11  14044  hashbccl  14056  ramlb  14072  0ram  14073  ramub1lem1  14079  ramub1lem2  14080  isstruct2  14175  lagsubg2  15733  lagsubg  15734  orbsta2  15823  symgbasfi  15882  symgfisg  15965  symggen2  15968  odcl2  16057  oddvds2  16058  sylow1lem2  16089  sylow1lem3  16090  sylow1lem4  16091  sylow1lem5  16092  odcau  16094  pgpssslw  16104  sylow2alem2  16108  sylow2a  16109  sylow2blem1  16110  sylow2blem3  16112  slwhash  16114  fislw  16115  sylow2  16116  sylow3lem1  16117  sylow3lem3  16119  sylow3lem4  16120  sylow3lem6  16122  cyggenod  16352  gsumval3OLD  16373  gsumval3lem1  16374  gsumval3lem2  16375  gsumval3  16376  gsumzadd  16400  gsumzaddOLD  16402  gsumzsplitOLD  16410  gsumzinvOLD  16433  gsumsubOLD  16438  gsumpt  16443  gsumptOLD  16444  gsum2dlem1  16449  gsum2dlem2  16450  gsum2d  16451  gsum2dOLD  16452  gsum2d2lem  16453  dprdfadd  16498  dprdfidOLD  16502  dprdfinvOLD  16504  dprdfaddOLD  16505  dmdprdsplitlemOLD  16523  dpjidclOLD  16552  ablfacrplem  16554  ablfacrp2  16556  ablfac1c  16560  ablfac1eulem  16561  ablfac1eu  16562  pgpfac1lem5  16568  pgpfaclem2  16571  pgpfaclem3  16572  ablfaclem3  16576  lcomfsupOLD  16962  lcomfsupp  16963  psrbaglecl  17414  psrbagaddcl  17415  psrbagaddclOLD  17416  psrbagcon  17417  psrbasOLD  17426  psrlidmOLD  17452  psrridmOLD  17454  mvridlemOLD  17469  mplsubg  17492  mpllss  17493  mplsubrglemOLD  17495  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  mplbas2OLD  17527  psrbagsn  17552  psrbagev1OLD  17570  evlslem6OLD  17574  psr1baslem  17616  funsnfsupOLD  17645  psgnghm2  17986  dsmmfi  18138  dsmmacl  18141  dsmmsubg  18143  dsmmlss  18144  frlmsslsp  18198  frlmsslspOLD  18199  mamures  18265  submabas  18364  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetralt  18389  maducoeval2  18421  madugsum  18424  fctop  18583  restfpw  18758  fincmp  18971  cmpfi  18986  bwth  18988  1stckgenlem  19101  ptbasfi  19129  ptcnplem  19169  ptcmpfi  19361  cfinfil  19441  ufinffr  19477  fin1aufil  19480  tsmsresOLD  19692  tsmsres  19693  xrge0gsumle  20385  xrge0tsms  20386  fsumcn  20421  rrxcph  20871  rrxmval  20879  ovoliunlem1  20960  ovolicc2lem4  20978  ovolicc2lem5  20979  i1fima  21131  i1fd  21134  itg1cl  21138  itg1ge0  21139  i1f0  21140  i1f1  21143  i1fadd  21148  i1fmul  21149  itg1addlem4  21152  i1fmulc  21156  itg1mulc  21157  i1fres  21158  itg10a  21163  itg1ge0a  21164  itg1climres  21167  mbfi1fseqlem4  21171  itgfsum  21279  dvmptfsum  21422  plyexmo  21754  aannenlem2  21770  aalioulem2  21774  birthday  22323  jensenlem1  22355  jensenlem2  22356  jensen  22357  wilthlem2  22382  ppifi  22418  prmdvdsfi  22420  0sgm  22457  sgmf  22458  sgmnncl  22460  ppiprm  22464  chtprm  22466  chtdif  22471  efchtdvds  22472  ppidif  22476  ppiltx  22490  mumul  22494  sqff1o  22495  fsumdvdsdiag  22499  fsumdvdscom  22500  dvdsflsumcom  22503  musum  22506  musumsum  22507  muinv  22508  fsumdvdsmul  22510  ppiub  22518  vmasum  22530  logfac2  22531  perfectlem2  22544  dchrfi  22569  dchrabs  22574  dchrptlem1  22578  dchrptlem2  22579  dchrpt  22581  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  chebbnd1lem1  22693  chtppilimlem1  22697  rplogsumlem2  22709  rpvmasumlem  22711  dchrvmasumlem1  22719  dchrisum0ff  22731  rpvmasum2  22736  dchrisum0re  22737  dchrisum0  22744  rplogsum  22751  dirith2  22752  vmalogdivsum2  22762  logsqvma  22766  logsqvma2  22767  selberg  22772  selberg34r  22795  pntsval2  22800  pntrlog2bndlem1  22801  cusgrafi  23341  vdgrfiun  23523  eupath2lem3  23551  konigsberg  23559  relfi  25891  unifi3  25956  ffsrn  25980  gsumunsnf  26196  gsumle  26197  xrge0tsmsd  26204  hasheuni  26486  sibfof  26678  sitgclg  26680  oddpwdc  26689  eulerpartlems  26695  eulerpartlemb  26703  eulerpartlemmf  26710  eulerpartlemgf  26714  eulerpartlemgs2  26715  coinfliplem  26813  coinflippv  26818  ballotlemfelz  26825  ballotlemfp1  26826  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemiex  26836  ballotlemsup  26839  ballotlemfg  26860  ballotlemfrc  26861  ballotlemfrceq  26863  ballotth  26872  deranglem  27006  subfacp1lem3  27022  subfacp1lem5  27024  subfacp1lem6  27025  erdszelem2  27032  erdszelem8  27038  erdsze2lem2  27044  snmlff  27170  fprod2dlem  27442  fprodcom2  27446  itg2addnclem2  28397  finminlem  28466  finlocfin  28524  lfinpfin  28528  locfincmp  28529  nnubfi  28599  nninfnub  28600  sstotbnd2  28626  cntotbnd  28648  rencldnfilem  29112  jm2.22  29297  jm2.23  29298  filnm  29396  phisum  29520  wwlknfi  30323  clwwlknfi  30430  qerclwwlknfi  30456  hashwwlkext  30518  ssnn0fi  30697  rmsuppfi  30737  mndpsuppfi  30739  scmsuppfi  30741  suppmptcfin  30743  mdetdiaglem  30824