Theorem ssfi 7742

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 7541	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7527	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5813	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5338	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5788	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3537	. . . . . . . . . . 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 7741	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7541	. . . . . . . . . . 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 5805	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5820	. . . . . . . . . . . . . 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 3098	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5307	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5797	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3187	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7527	. . . . . . . . . . . . . . 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 7569	. . . . . . . . . . . . . 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 2917	. . . . . . . . . 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 7541	. . . . . . . . . 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 1711	. . . . 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 2929	. . 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 1599   e. wcel 1804   E.wrex 2794   C_ wss 3461   class class class wbr 4437   ran crn 4990   |` cres 4991   "cima 4992   -1-1->wf1 5575   -onto->wfo 5576   -1-1-onto->wf1o 5577   omcom 6685   ~~ cen 7515   Fincfn 7518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-om 6686  df-er 7313  df-en 7519  df-fin 7522

This theorem is referenced by:  domfi  7743  infi  7745  finresfin  7747  diffi  7753  findcard3  7765  unfir  7790  fnfi  7800  fofinf1o  7803  cnvfi  7806  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  wemapso2OLD  7980  wemapso2lem  7981  cantnfp1lem1  8100  oemapvali  8106  cantnfp1lem1OLD  8126  cantnflem1dOLD  8133  cantnflem1OLD  8134  mapfienOLD  8141  ackbij2lem1  8602  ackbij1lem11  8613  fin23lem26  8708  fin23lem23  8709  fin23lem21  8722  fin11a  8766  isfin1-3  8769  axcclem  8840  pwfseqlem4  9043  ssnn0fi  12076  hashun3  12434  hashss  12456  hashssdif  12457  hashsslei  12466  hashbclem  12483  hashf1lem2  12487  seqcoll2  12495  pr2pwpr  12502  isercolllem2  13470  isercoll  13472  fsum2dlem  13567  fsumcom2  13571  fsumless  13592  fsumabs  13597  fsumrlim  13607  fsumo1  13608  cvgcmpce  13614  fsumiun  13617  qshash  13621  incexclem  13630  incexc  13631  incexc2  13632  fprod2dlem  13766  fprodcom2  13770  bitsfi  14069  bitsinv1  14074  bitsinvp1  14081  sadcaddlem  14089  sadadd2lem  14091  sadadd3  14093  sadaddlem  14098  sadasslem  14102  sadeq  14104  phicl2  14280  phibnd  14283  hashdvds  14287  phiprmpw  14288  phimullem  14291  eulerthlem2  14294  eulerth  14295  sumhash  14397  prmreclem2  14417  prmreclem3  14418  prmreclem4  14419  prmreclem5  14420  1arith  14427  4sqlem11  14455  vdwlem11  14491  hashbccl  14503  ramlb  14519  0ram  14520  ramub1lem1  14526  ramub1lem2  14527  isstruct2  14623  lagsubg2  16241  lagsubg  16242  orbsta2  16331  symgbasfi  16390  symgfisg  16472  symggen2  16475  odcl2  16566  oddvds2  16567  sylow1lem2  16598  sylow1lem3  16599  sylow1lem4  16600  sylow1lem5  16601  odcau  16603  pgpssslw  16613  sylow2alem2  16617  sylow2a  16618  sylow2blem1  16619  sylow2blem3  16621  slwhash  16623  fislw  16624  sylow2  16625  sylow3lem1  16626  sylow3lem3  16628  sylow3lem4  16629  sylow3lem6  16631  cyggenod  16866  gsumval3OLD  16887  gsumval3lem1  16888  gsumval3lem2  16889  gsumval3  16890  gsumzadd  16914  gsumzaddOLD  16916  gsumzsplitOLD  16924  gsumzinvOLD  16949  gsumsubOLD  16954  gsumpt  16967  gsumptOLD  16968  gsum2dlem1  16976  gsum2dlem2  16977  gsum2d  16978  gsum2dOLD  16979  gsum2d2lem  16980  dprdfadd  17039  dprdfidOLD  17043  dprdfinvOLD  17045  dprdfaddOLD  17046  dmdprdsplitlemOLD  17064  dpjidclOLD  17093  ablfacrplem  17095  ablfacrp2  17097  ablfac1c  17101  ablfac1eulem  17102  ablfac1eu  17103  pgpfac1lem5  17109  pgpfaclem2  17112  pgpfaclem3  17113  ablfaclem3  17117  lcomfsupOLD  17528  lcomfsupp  17529  psrbaglecl  17998  psrbagaddcl  17999  psrbagaddclOLD  18000  psrbagcon  18001  psrbasOLD  18010  psrlidmOLD  18036  psrridmOLD  18038  mvridlemOLD  18054  mplsubg  18077  mpllss  18078  mplsubrglemOLD  18080  mplcoe3OLD  18108  mplcoe5  18110  mplcoe2OLD  18112  mplbas2OLD  18114  psrbagsn  18139  psrbagev1OLD  18157  evlslem6OLD  18161  psr1baslem  18203  funsnfsupOLD  18235  dsmmfi  18747  dsmmacl  18750  dsmmsubg  18752  dsmmlss  18753  frlmsslsp  18807  frlmsslspOLD  18808  mamures  18870  submabas  19058  mdetdiaglem  19078  mdetrlin  19082  mdetrsca  19083  mdetralt  19088  maducoeval2  19120  madugsum  19123  fctop  19483  restfpw  19658  fincmp  19871  cmpfi  19886  bwth  19888  finlocfin  19999  lfinpfin  20003  locfincmp  20005  1stckgenlem  20032  ptbasfi  20060  ptcnplem  20100  ptcmpfi  20292  cfinfil  20372  ufinffr  20408  fin1aufil  20411  tsmsresOLD  20623  tsmsres  20624  xrge0gsumle  21316  xrge0tsms  21317  fsumcn  21352  rrxcph  21802  rrxmval  21810  ovoliunlem1  21891  ovolicc2lem4  21909  ovolicc2lem5  21910  i1fima  22063  i1fd  22066  itg1cl  22070  itg1ge0  22071  i1f0  22072  i1f1  22075  i1fadd  22080  i1fmul  22081  itg1addlem4  22084  i1fmulc  22088  itg1mulc  22089  i1fres  22090  itg10a  22095  itg1ge0a  22096  itg1climres  22099  mbfi1fseqlem4  22103  itgfsum  22211  dvmptfsum  22354  plyexmo  22687  aannenlem2  22703  aalioulem2  22707  birthday  23262  jensenlem1  23294  jensenlem2  23295  jensen  23296  wilthlem2  23321  ppifi  23357  prmdvdsfi  23359  0sgm  23396  sgmf  23397  sgmnncl  23399  ppiprm  23403  chtprm  23405  chtdif  23410  efchtdvds  23411  ppidif  23415  ppiltx  23429  mumul  23433  sqff1o  23434  fsumdvdsdiag  23438  fsumdvdscom  23439  dvdsflsumcom  23442  musum  23445  musumsum  23446  muinv  23447  fsumdvdsmul  23449  ppiub  23457  vmasum  23469  logfac2  23470  perfectlem2  23483  dchrfi  23508  dchrabs  23513  dchrptlem1  23517  dchrptlem2  23518  dchrpt  23520  lgsquadlem1  23607  lgsquadlem2  23608  lgsquadlem3  23609  chebbnd1lem1  23632  chtppilimlem1  23636  rplogsumlem2  23648  rpvmasumlem  23650  dchrvmasumlem1  23658  dchrisum0ff  23670  rpvmasum2  23675  dchrisum0re  23676  dchrisum0  23683  rplogsum  23690  dirith2  23691  vmalogdivsum2  23701  logsqvma  23705  logsqvma2  23706  selberg  23711  selberg34r  23734  pntsval2  23739  pntrlog2bndlem1  23740  cusgrafi  24460  wwlknfi  24716  hashwwlkext  24724  clwwlknfi  24756  qerclwwlknfi  24807  vdgrfiun  24880  eupath2lem3  24957  konigsberg  24965  relfi  27437  unifi3  27506  ffsrn  27530  gsumle  27748  xrge0tsmsd  27753  hasheuni  28069  sibfof  28260  sitgclg  28262  oddpwdc  28271  eulerpartlems  28277  eulerpartlemb  28285  eulerpartlemmf  28292  eulerpartlemgf  28296  eulerpartlemgs2  28297  coinfliplem  28395  coinflippv  28400  ballotlemfelz  28407  ballotlemfp1  28408  ballotlemfc0  28409  ballotlemfcc  28410  ballotlemiex  28418  ballotlemsup  28421  ballotlemfg  28442  ballotlemfrc  28443  ballotlemfrceq  28445  ballotth  28454  deranglem  28588  subfacp1lem3  28604  subfacp1lem5  28606  subfacp1lem6  28607  erdszelem2  28614  erdszelem8  28620  erdsze2lem2  28626  snmlff  28752  mvrsfpw  28844  itg2addnclem2  30043  finminlem  30112  nnubfi  30219  nninfnub  30220  sstotbnd2  30246  cntotbnd  30268  rencldnfilem  30730  jm2.22  30913  jm2.23  30914  filnm  31012  phisum  31135  fprodexp  31554  fprodabs2  31556  mccllem  31559  sumnnodd  31590  fprodcncf  31658  dvmptfprod  31696  dvnprodlem1  31697  dvnprodlem2  31698  fourierdlem25  31868  fourierdlem37  31880  fourierdlem51  31894  fourierdlem79  31922  fouriersw  31968  etransclem16  31987  etransclem24  31995  etransclem31  32002  etransclem32  32003  etransclem33  32004  etransclem34  32005  etransclem37  32008  etransclem44  32015  rmsuppfi  32836  mndpsuppfi  32838  scmsuppfi  32840  suppmptcfin  32842