Theorem ssfi 7737

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 7536	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7522	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5821	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5346	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5796	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3552	. . . . . . . . . . 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 7736	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7536	. . . . . . . . . . 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 5813	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5828	. . . . . . . . . . . . . 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 3116	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5315	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5805	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3205	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7522	. . . . . . . . . . . . . . 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 7564	. . . . . . . . . . . . . 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 2937	. . . . . . . . . 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 7536	. . . . . . . . . 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 1700	. . . . 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 2949	. . 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 1596   e. wcel 1767   E.wrex 2815   C_ wss 3476   class class class wbr 4447   ran crn 5000   |` cres 5001   "cima 5002   -1-1->wf1 5583   -onto->wfo 5584   -1-1-onto->wf1o 5585   omcom 6678   ~~ cen 7510   Fincfn 7513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-om 6679  df-er 7308  df-en 7514  df-fin 7517

This theorem is referenced by:  domfi  7738  infi  7740  finresfin  7742  diffi  7747  findcard3  7759  unfir  7784  fnfi  7794  fofinf1o  7797  cnvfi  7800  f1fi  7803  imafi  7809  mapfi  7812  ixpfi  7813  ixpfi2  7814  mptfi  7815  cnvimamptfin  7817  fisuppfi  7833  suppssfifsupp  7840  fsuppunbi  7846  snopfsupp  7848  fsuppres  7850  ressuppfi  7851  fsuppmptif  7855  fsuppco2  7858  fsuppcor  7859  sniffsupp  7865  elfiun  7886  marypha1lem  7889  wemapso2OLD  7973  wemapso2lem  7974  cantnfp1lem1  8093  oemapvali  8099  cantnfp1lem1OLD  8119  cantnflem1dOLD  8126  cantnflem1OLD  8127  mapfienOLD  8134  ackbij2lem1  8595  ackbij1lem11  8606  fin23lem26  8701  fin23lem23  8702  fin23lem21  8715  fin11a  8759  isfin1-3  8762  axcclem  8833  pwfseqlem4  9036  ssnn0fi  12057  hashun3  12414  hashss  12433  hashssdif  12434  hashsslei  12443  hashbclem  12461  hashf1lem2  12465  seqcoll2  12473  pr2pwpr  12480  isercolllem2  13444  isercoll  13446  fsumss  13503  fsum2dlem  13541  fsumcom2  13545  fsumless  13566  fsumabs  13571  fsumrlim  13581  fsumo1  13582  cvgcmpce  13588  fsumiun  13591  qshash  13595  incexclem  13604  incexc  13605  incexc2  13606  bitsfi  13939  bitsinv1  13944  bitsinvp1  13951  sadcaddlem  13959  sadadd2lem  13961  sadadd3  13963  sadaddlem  13968  sadasslem  13972  sadeq  13974  phicl2  14150  phibnd  14153  hashdvds  14157  phiprmpw  14158  phimullem  14161  eulerthlem2  14164  eulerth  14165  sumhash  14267  prmreclem2  14287  prmreclem3  14288  prmreclem4  14289  prmreclem5  14290  1arith  14297  4sqlem11  14325  vdwlem11  14361  hashbccl  14373  ramlb  14389  0ram  14390  ramub1lem1  14396  ramub1lem2  14397  isstruct2  14492  lagsubg2  16054  lagsubg  16055  orbsta2  16144  symgbasfi  16203  symgfisg  16286  symggen2  16289  odcl2  16380  oddvds2  16381  sylow1lem2  16412  sylow1lem3  16413  sylow1lem4  16414  sylow1lem5  16415  odcau  16417  pgpssslw  16427  sylow2alem2  16431  sylow2a  16432  sylow2blem1  16433  sylow2blem3  16435  slwhash  16437  fislw  16438  sylow2  16439  sylow3lem1  16440  sylow3lem3  16442  sylow3lem4  16443  sylow3lem6  16445  cyggenod  16675  gsumval3OLD  16696  gsumval3lem1  16697  gsumval3lem2  16698  gsumval3  16699  gsumzadd  16723  gsumzaddOLD  16725  gsumzsplitOLD  16733  gsumzinvOLD  16758  gsumsubOLD  16763  gsumpt  16776  gsumptOLD  16777  gsum2dlem1  16785  gsum2dlem2  16786  gsum2d  16787  gsum2dOLD  16788  gsum2d2lem  16789  dprdfadd  16847  dprdfidOLD  16851  dprdfinvOLD  16853  dprdfaddOLD  16854  dmdprdsplitlemOLD  16872  dpjidclOLD  16901  ablfacrplem  16903  ablfacrp2  16905  ablfac1c  16909  ablfac1eulem  16910  ablfac1eu  16911  pgpfac1lem5  16917  pgpfaclem2  16920  pgpfaclem3  16921  ablfaclem3  16925  lcomfsupOLD  17329  lcomfsupp  17330  psrbaglecl  17787  psrbagaddcl  17788  psrbagaddclOLD  17789  psrbagcon  17790  psrbasOLD  17799  psrlidmOLD  17825  psrridmOLD  17827  mvridlemOLD  17843  mplsubg  17866  mpllss  17867  mplsubrglemOLD  17869  mplcoe3OLD  17897  mplcoe5  17899  mplcoe2OLD  17901  mplbas2OLD  17903  psrbagsn  17928  psrbagev1OLD  17946  evlslem6OLD  17950  psr1baslem  17992  funsnfsupOLD  18024  psgnghm2  18381  dsmmfi  18533  dsmmacl  18536  dsmmsubg  18538  dsmmlss  18539  frlmsslsp  18593  frlmsslspOLD  18594  mamures  18656  submabas  18844  mdetdiaglem  18864  mdetrlin  18868  mdetrsca  18869  mdetralt  18874  maducoeval2  18906  madugsum  18909  fctop  19268  restfpw  19443  fincmp  19656  cmpfi  19671  bwth  19673  1stckgenlem  19786  ptbasfi  19814  ptcnplem  19854  ptcmpfi  20046  cfinfil  20126  ufinffr  20162  fin1aufil  20165  tsmsresOLD  20377  tsmsres  20378  xrge0gsumle  21070  xrge0tsms  21071  fsumcn  21106  rrxcph  21556  rrxmval  21564  ovoliunlem1  21645  ovolicc2lem4  21663  ovolicc2lem5  21664  i1fima  21817  i1fd  21820  itg1cl  21824  itg1ge0  21825  i1f0  21826  i1f1  21829  i1fadd  21834  i1fmul  21835  itg1addlem4  21838  i1fmulc  21842  itg1mulc  21843  i1fres  21844  itg10a  21849  itg1ge0a  21850  itg1climres  21853  mbfi1fseqlem4  21857  itgfsum  21965  dvmptfsum  22108  plyexmo  22440  aannenlem2  22456  aalioulem2  22460  birthday  23009  jensenlem1  23041  jensenlem2  23042  jensen  23043  wilthlem2  23068  ppifi  23104  prmdvdsfi  23106  0sgm  23143  sgmf  23144  sgmnncl  23146  ppiprm  23150  chtprm  23152  chtdif  23157  efchtdvds  23158  ppidif  23162  ppiltx  23176  mumul  23180  sqff1o  23181  fsumdvdsdiag  23185  fsumdvdscom  23186  dvdsflsumcom  23189  musum  23192  musumsum  23193  muinv  23194  fsumdvdsmul  23196  ppiub  23204  vmasum  23216  logfac2  23217  perfectlem2  23230  dchrfi  23255  dchrabs  23260  dchrptlem1  23264  dchrptlem2  23265  dchrpt  23267  lgsquadlem1  23354  lgsquadlem2  23355  lgsquadlem3  23356  chebbnd1lem1  23379  chtppilimlem1  23383  rplogsumlem2  23395  rpvmasumlem  23397  dchrvmasumlem1  23405  dchrisum0ff  23417  rpvmasum2  23422  dchrisum0re  23423  dchrisum0  23430  rplogsum  23437  dirith2  23438  vmalogdivsum2  23448  logsqvma  23452  logsqvma2  23453  selberg  23458  selberg34r  23481  pntsval2  23486  pntrlog2bndlem1  23487  cusgrafi  24155  wwlknfi  24411  hashwwlkext  24419  clwwlknfi  24451  qerclwwlknfi  24502  vdgrfiun  24575  eupath2lem3  24652  konigsberg  24660  relfi  27129  unifi3  27197  ffsrn  27221  gsumle  27430  xrge0tsmsd  27435  hasheuni  27728  sibfof  27919  sitgclg  27921  oddpwdc  27930  eulerpartlems  27936  eulerpartlemb  27944  eulerpartlemmf  27951  eulerpartlemgf  27955  eulerpartlemgs2  27956  coinfliplem  28054  coinflippv  28059  ballotlemfelz  28066  ballotlemfp1  28067  ballotlemfc0  28068  ballotlemfcc  28069  ballotlemiex  28077  ballotlemsup  28080  ballotlemfg  28101  ballotlemfrc  28102  ballotlemfrceq  28104  ballotth  28113  deranglem  28247  subfacp1lem3  28263  subfacp1lem5  28265  subfacp1lem6  28266  erdszelem2  28273  erdszelem8  28279  erdsze2lem2  28285  snmlff  28411  fprod2dlem  28684  fprodcom2  28688  itg2addnclem2  29642  finminlem  29711  finlocfin  29769  lfinpfin  29773  locfincmp  29774  nnubfi  29844  nninfnub  29845  sstotbnd2  29871  cntotbnd  29893  rencldnfilem  30356  jm2.22  30541  jm2.23  30542  filnm  30640  phisum  30764  hashssle  31074  sumnnodd  31172  fourierdlem25  31432  fourierdlem37  31444  fourierdlem51  31458  fourierdlem79  31486  fouriersw  31532  rmsuppfi  32039  mndpsuppfi  32041  scmsuppfi  32043  suppmptcfin  32045