Theorem ssfi 7521

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 7321	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7307	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5636	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5168	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5611	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3392	. . . . . . . . . . 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 7520	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7321	. . . . . . . . . . 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 471	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 709	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5628	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5643	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 468	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 2965	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5138	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5620	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3053	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7307	. . . . . . . . . . . . . . 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 7349	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 468	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 468	. . . . . . . . . . . 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 2817	. . . . . . . . . 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 7321	. . . . . . . . . 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 463	. . . . . . . 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 600	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1689	. . . . 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 2825	. . 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 1589   e. wcel 1755   E.wrex 2706   C_ wss 3316   class class class wbr 4280   ran crn 4828   |` cres 4829   "cima 4830   -1-1->wf1 5403   -onto->wfo 5404   -1-1-onto->wf1o 5405   omcom 6465   ~~ cen 7295   Fincfn 7298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-om 6466  df-er 7089  df-en 7299  df-fin 7302

This theorem is referenced by:  domfi  7522  infi  7524  finresfin  7526  diffi  7531  findcard3  7543  unfir  7568  fnfi  7577  fofinf1o  7580  cnvfi  7583  f1fi  7586  imafi  7592  mapfi  7595  ixpfi  7596  ixpfi2  7597  mptfi  7598  cnvimamptfin  7600  fisuppfi  7616  suppssfifsupp  7623  fsuppunbi  7629  snopfsupp  7631  fsuppres  7633  ressuppfi  7634  fsuppmptif  7637  fsuppco2  7640  fsuppcor  7641  sniffsupp  7647  elfiun  7668  marypha1lem  7671  wemapso2OLD  7754  wemapso2lem  7755  cantnfp1lem1  7874  oemapvali  7880  cantnfp1lem1OLD  7900  cantnflem1dOLD  7907  cantnflem1OLD  7908  mapfienOLD  7915  ackbij2lem1  8376  ackbij1lem11  8387  fin23lem26  8482  fin23lem23  8483  fin23lem21  8496  fin11a  8540  isfin1-3  8543  axcclem  8614  pwfseqlem4  8817  hashun3  12131  hashss  12150  hashssdif  12151  hashsslei  12160  pr2pwpr  12167  hashbclem  12189  hashf1lem2  12193  seqcoll2  12201  isercolllem2  13127  isercoll  13129  fsumss  13186  fsum2dlem  13221  fsumcom2  13225  fsumless  13242  fsumabs  13247  fsumrlim  13257  fsumo1  13258  cvgcmpce  13264  fsumiun  13267  qshash  13273  incexclem  13282  incexc  13283  incexc2  13284  bitsfi  13616  bitsinv1  13621  bitsinvp1  13628  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  sadasslem  13649  sadeq  13651  phicl2  13826  phibnd  13829  hashdvds  13833  phiprmpw  13834  phimullem  13837  eulerthlem2  13840  eulerth  13841  sumhash  13941  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem5  13964  1arith  13971  4sqlem11  13999  vdwlem11  14035  hashbccl  14047  ramlb  14063  0ram  14064  ramub1lem1  14070  ramub1lem2  14071  isstruct2  14166  lagsubg2  15722  lagsubg  15723  orbsta2  15812  symgbasfi  15871  symgfisg  15954  symggen2  15957  odcl2  16046  oddvds2  16047  sylow1lem2  16078  sylow1lem3  16079  sylow1lem4  16080  sylow1lem5  16081  odcau  16083  pgpssslw  16093  sylow2alem2  16097  sylow2a  16098  sylow2blem1  16099  sylow2blem3  16101  slwhash  16103  fislw  16104  sylow2  16105  sylow3lem1  16106  sylow3lem3  16108  sylow3lem4  16109  sylow3lem6  16111  cyggenod  16341  gsumval3OLD  16362  gsumval3lem1  16363  gsumval3lem2  16364  gsumval3  16365  gsumzadd  16389  gsumzaddOLD  16391  gsumzsplitOLD  16399  gsumzinvOLD  16419  gsumsubOLD  16424  gsumpt  16429  gsumptOLD  16430  gsum2dlem1  16435  gsum2dlem2  16436  gsum2d  16437  gsum2dOLD  16438  gsum2d2lem  16439  dprdfadd  16484  dprdfidOLD  16488  dprdfinvOLD  16490  dprdfaddOLD  16491  dmdprdsplitlemOLD  16509  dpjidclOLD  16538  ablfacrplem  16540  ablfacrp2  16542  ablfac1c  16546  ablfac1eulem  16547  ablfac1eu  16548  pgpfac1lem5  16554  pgpfaclem2  16557  pgpfaclem3  16558  ablfaclem3  16562  lcomfsupOLD  16908  lcomfsupp  16909  psrbaglecl  17371  psrbagaddcl  17372  psrbagaddclOLD  17373  psrbagcon  17374  psrbasOLD  17383  psrlidmOLD  17409  psrridmOLD  17411  mvridlemOLD  17426  mplsubg  17449  mpllss  17450  mplsubrglemOLD  17452  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  mplbas2OLD  17484  psrbagsn  17509  psrbagev1OLD  17523  psr1baslem  17540  funsnfsupOLD  17569  psgnghm2  17853  dsmmfi  18005  dsmmacl  18008  dsmmsubg  18010  dsmmlss  18011  frlmsslsp  18065  frlmsslspOLD  18066  mamures  18132  submabas  18231  mdet1  18250  mdetrlin  18251  mdetrsca  18252  mdetralt  18256  maducoeval2  18288  madugsum  18291  fctop  18450  restfpw  18625  fincmp  18838  cmpfi  18853  bwth  18855  1stckgenlem  18968  ptbasfi  18996  ptcnplem  19036  ptcmpfi  19228  cfinfil  19308  ufinffr  19344  fin1aufil  19347  tsmsresOLD  19559  tsmsres  19560  xrge0gsumle  20252  xrge0tsms  20253  fsumcn  20288  rrxcph  20738  rrxmval  20746  ovoliunlem1  20827  ovolicc2lem4  20845  ovolicc2lem5  20846  i1fima  20998  i1fd  21001  itg1cl  21005  itg1ge0  21006  i1f0  21007  i1f1  21010  i1fadd  21015  i1fmul  21016  itg1addlem4  21019  i1fmulc  21023  itg1mulc  21024  i1fres  21025  itg10a  21030  itg1ge0a  21031  itg1climres  21034  mbfi1fseqlem4  21038  itgfsum  21146  dvmptfsum  21289  evlslem6OLD  21365  plyexmo  21664  aannenlem2  21680  aalioulem2  21684  birthday  22233  jensenlem1  22265  jensenlem2  22266  jensen  22267  wilthlem2  22292  ppifi  22328  prmdvdsfi  22330  0sgm  22367  sgmf  22368  sgmnncl  22370  ppiprm  22374  chtprm  22376  chtdif  22381  efchtdvds  22382  ppidif  22386  ppiltx  22400  mumul  22404  sqff1o  22405  fsumdvdsdiag  22409  fsumdvdscom  22410  dvdsflsumcom  22413  musum  22416  musumsum  22417  muinv  22418  fsumdvdsmul  22420  ppiub  22428  vmasum  22440  logfac2  22441  perfectlem2  22454  dchrfi  22479  dchrabs  22484  dchrptlem1  22488  dchrptlem2  22489  dchrpt  22491  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  chebbnd1lem1  22603  chtppilimlem1  22607  rplogsumlem2  22619  rpvmasumlem  22621  dchrvmasumlem1  22629  dchrisum0ff  22641  rpvmasum2  22646  dchrisum0re  22647  dchrisum0  22654  rplogsum  22661  dirith2  22662  vmalogdivsum2  22672  logsqvma  22676  logsqvma2  22677  selberg  22682  selberg34r  22705  pntsval2  22710  pntrlog2bndlem1  22711  cusgrafi  23213  vdgrfiun  23395  eupath2lem3  23423  konigsberg  23431  relfi  25764  unifi3  25829  ffsrn  25854  gsumunsnf  26097  gsumle  26098  xrge0tsmsd  26106  hasheuni  26388  sibfof  26574  sitgclg  26576  oddpwdc  26585  eulerpartlems  26591  eulerpartlemb  26599  eulerpartlemmf  26606  eulerpartlemgf  26610  eulerpartlemgs2  26611  coinfliplem  26709  coinflippv  26714  ballotlemfelz  26721  ballotlemfp1  26722  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemiex  26732  ballotlemsup  26735  ballotlemfg  26756  ballotlemfrc  26757  ballotlemfrceq  26759  ballotth  26768  deranglem  26902  subfacp1lem3  26918  subfacp1lem5  26920  subfacp1lem6  26921  erdszelem2  26928  erdszelem8  26934  erdsze2lem2  26940  snmlff  27066  fprod2dlem  27338  fprodcom2  27342  itg2addnclem2  28288  finminlem  28357  finlocfin  28415  lfinpfin  28419  locfincmp  28420  nnubfi  28490  nninfnub  28491  sstotbnd2  28517  cntotbnd  28539  rencldnfilem  29004  jm2.22  29189  jm2.23  29190  filnm  29288  phisum  29412  wwlknfi  30216  clwwlknfi  30323  qerclwwlknfi  30349  hashwwlkext  30411  rmsuppfi  30617  mndpsuppfi  30619  scmsuppfi  30621  suppmptcfin  30623