Theorem ssfi 7656

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 7458	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7444	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5731	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5260	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5706	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3465	. . . . . . . . . . 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 7655	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7458	. . . . . . . . . . 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 472	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 714	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5723	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5738	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 469	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 3037	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5229	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5715	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3126	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7444	. . . . . . . . . . . . . . 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 7486	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 469	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 469	. . . . . . . . . . . 12 |- ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25	24	ex 432	. . . . . . . . . . 11 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26	25	reximdv 2856	. . . . . . . . . 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 7458	. . . . . . . . . 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 464	. . . . . . . 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 603	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1732	. . . . 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 2868	. . 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 427	1 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   /\ wa 367   E.wex 1620   e. wcel 1826   E.wrex 2733   C_ wss 3389   class class class wbr 4367   ran crn 4914   |` cres 4915   "cima 4916   -1-1->wf1 5493   -onto->wfo 5494   -1-1-onto->wf1o 5495   omcom 6599   ~~ cen 7432   Fincfn 7435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-om 6600  df-er 7229  df-en 7436  df-fin 7439

This theorem is referenced by:  domfi  7657  infi  7659  finresfin  7661  diffi  7667  findcard3  7678  unfir  7703  fnfi  7713  fofinf1o  7716  cnvfi  7719  f1fi  7722  imafi  7728  mapfi  7731  ixpfi  7732  ixpfi2  7733  mptfi  7734  cnvimamptfin  7736  fisuppfi  7752  suppssfifsupp  7759  fsuppunbi  7765  snopfsupp  7767  fsuppres  7769  ressuppfi  7770  fsuppmptif  7774  fsuppco2  7777  fsuppcor  7778  sniffsupp  7784  elfiun  7805  marypha1lem  7808  wemapso2OLD  7892  wemapso2lem  7893  cantnfp1lem1  8010  oemapvali  8016  cantnfp1lem1OLD  8036  cantnflem1dOLD  8043  cantnflem1OLD  8044  mapfienOLD  8051  ackbij2lem1  8512  ackbij1lem11  8523  fin23lem26  8618  fin23lem23  8619  fin23lem21  8632  fin11a  8676  isfin1-3  8679  axcclem  8750  pwfseqlem4  8951  ssnn0fi  11997  hashun3  12355  hashss  12378  hashssdif  12379  hashsslei  12388  hashbclem  12405  hashf1lem2  12409  seqcoll2  12417  pr2pwpr  12424  isercolllem2  13490  isercoll  13492  fsum2dlem  13587  fsumcom2  13591  fsumless  13612  fsumabs  13617  fsumrlim  13627  fsumo1  13628  cvgcmpce  13634  fsumiun  13637  qshash  13641  incexclem  13650  incexc  13651  incexc2  13652  fprod2dlem  13786  fprodcom2  13790  bitsfi  14089  bitsinv1  14094  bitsinvp1  14101  sadcaddlem  14109  sadadd2lem  14111  sadadd3  14113  sadaddlem  14118  sadasslem  14122  sadeq  14124  phicl2  14300  phibnd  14303  hashdvds  14307  phiprmpw  14308  phimullem  14311  eulerthlem2  14314  eulerth  14315  sumhash  14417  prmreclem2  14437  prmreclem3  14438  prmreclem4  14439  prmreclem5  14440  1arith  14447  4sqlem11  14475  vdwlem11  14511  hashbccl  14523  ramlb  14539  0ram  14540  ramub1lem1  14546  ramub1lem2  14547  isstruct2  14643  lagsubg2  16379  lagsubg  16380  orbsta2  16469  symgbasfi  16528  symgfisg  16610  symggen2  16613  odcl2  16704  oddvds2  16705  sylow1lem2  16736  sylow1lem3  16737  sylow1lem4  16738  sylow1lem5  16739  odcau  16741  pgpssslw  16751  sylow2alem2  16755  sylow2a  16756  sylow2blem1  16757  sylow2blem3  16759  slwhash  16761  fislw  16762  sylow2  16763  sylow3lem1  16764  sylow3lem3  16766  sylow3lem4  16767  sylow3lem6  16769  cyggenod  17004  gsumval3OLD  17025  gsumval3lem1  17026  gsumval3lem2  17027  gsumval3  17028  gsumzadd  17052  gsumzaddOLD  17054  gsumzsplitOLD  17062  gsumzinvOLD  17086  gsumpt  17102  gsumptOLD  17103  gsum2dlem1  17111  gsum2dlem2  17112  gsum2d  17113  gsum2dOLD  17114  gsum2d2lem  17115  dprdfadd  17173  dprdfidOLD  17177  dprdfinvOLD  17179  dprdfaddOLD  17180  dmdprdsplitlemOLD  17198  dpjidclOLD  17227  ablfacrplem  17229  ablfacrp2  17231  ablfac1c  17235  ablfac1eulem  17236  ablfac1eu  17237  pgpfac1lem5  17243  pgpfaclem2  17246  pgpfaclem3  17247  ablfaclem3  17251  lcomfsupOLD  17662  lcomfsupp  17663  psrbaglecl  18132  psrbagaddcl  18133  psrbagaddclOLD  18134  psrbagcon  18135  psrbasOLD  18144  psrlidmOLD  18170  psrridmOLD  18172  mvridlemOLD  18188  mplsubg  18211  mpllss  18212  mplsubrglemOLD  18214  mplcoe3OLD  18242  mplcoe5  18244  mplcoe2OLD  18246  mplbas2OLD  18248  psrbagsn  18273  psrbagev1OLD  18291  evlslem6OLD  18295  psr1baslem  18337  funsnfsupOLD  18369  dsmmfi  18860  dsmmacl  18863  dsmmsubg  18865  dsmmlss  18866  frlmsslsp  18916  mamures  18977  submabas  19165  mdetdiaglem  19185  mdetrlin  19189  mdetrsca  19190  mdetralt  19195  maducoeval2  19227  madugsum  19230  fctop  19590  restfpw  19766  fincmp  19979  cmpfi  19994  bwth  19996  finlocfin  20106  lfinpfin  20110  locfincmp  20112  1stckgenlem  20139  ptbasfi  20167  ptcnplem  20207  ptcmpfi  20399  cfinfil  20479  ufinffr  20515  fin1aufil  20518  tsmsresOLD  20730  tsmsres  20731  xrge0gsumle  21423  xrge0tsms  21424  fsumcn  21459  rrxcph  21909  rrxmval  21917  ovoliunlem1  21998  ovolicc2lem4  22016  ovolicc2lem5  22017  i1fima  22170  i1fd  22173  itg1cl  22177  itg1ge0  22178  i1f0  22179  i1f1  22182  i1fadd  22187  i1fmul  22188  itg1addlem4  22191  i1fmulc  22195  itg1mulc  22196  i1fres  22197  itg10a  22202  itg1ge0a  22203  itg1climres  22206  mbfi1fseqlem4  22210  itgfsum  22318  dvmptfsum  22461  plyexmo  22794  aannenlem2  22810  aalioulem2  22814  birthday  23401  jensenlem1  23433  jensenlem2  23434  jensen  23435  wilthlem2  23460  ppifi  23496  prmdvdsfi  23498  0sgm  23535  sgmf  23536  sgmnncl  23538  ppiprm  23542  chtprm  23544  chtdif  23549  efchtdvds  23550  ppidif  23554  ppiltx  23568  mumul  23572  sqff1o  23573  fsumdvdsdiag  23577  fsumdvdscom  23578  dvdsflsumcom  23581  musum  23584  musumsum  23585  muinv  23586  fsumdvdsmul  23588  ppiub  23596  vmasum  23608  logfac2  23609  perfectlem2  23622  dchrfi  23647  dchrabs  23652  dchrptlem1  23656  dchrptlem2  23657  dchrpt  23659  lgsquadlem1  23746  lgsquadlem2  23747  lgsquadlem3  23748  chebbnd1lem1  23771  chtppilimlem1  23775  rplogsumlem2  23787  rpvmasumlem  23789  dchrvmasumlem1  23797  dchrisum0ff  23809  rpvmasum2  23814  dchrisum0re  23815  dchrisum0  23822  rplogsum  23829  dirith2  23830  vmalogdivsum2  23840  logsqvma  23844  logsqvma2  23845  selberg  23850  selberg34r  23873  pntsval2  23878  pntrlog2bndlem1  23879  cusgrafi  24603  wwlknfi  24859  hashwwlkext  24867  clwwlknfi  24899  qerclwwlknfi  24950  vdgrfiun  25023  eupath2lem3  25100  konigsberg  25108  relfi  27592  imafi2  27676  unifi3  27677  ffsrn  27702  gsumle  27923  xrge0tsmsd  27929  hasheuni  28233  carsgclctunlem1  28444  sibfof  28465  sitgclg  28467  oddpwdc  28476  eulerpartlems  28482  eulerpartlemb  28490  eulerpartlemmf  28497  eulerpartlemgf  28501  eulerpartlemgs2  28502  coinfliplem  28600  coinflippv  28605  ballotlemfelz  28612  ballotlemfp1  28613  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemiex  28623  ballotlemsup  28626  ballotlemfg  28647  ballotlemfrc  28648  ballotlemfrceq  28650  ballotth  28659  deranglem  28799  subfacp1lem3  28815  subfacp1lem5  28817  subfacp1lem6  28818  erdszelem2  28825  erdszelem8  28831  erdsze2lem2  28837  snmlff  28963  mvrsfpw  29055  itg2addnclem2  30233  finminlem  30302  nnubfi  30409  nninfnub  30410  sstotbnd2  30436  cntotbnd  30458  rencldnfilem  30919  jm2.22  31103  jm2.23  31104  filnm  31202  phisum  31327  fprodexp  31766  fprodabs2  31768  mccllem  31771  sumnnodd  31802  fprodcncf  31870  dvmptfprod  31908  dvnprodlem1  31909  dvnprodlem2  31910  fourierdlem25  32080  fourierdlem37  32092  fourierdlem51  32106  fourierdlem79  32134  fouriersw  32180  etransclem16  32199  etransclem24  32207  etransclem33  32216  etransclem44  32227  perfectALTVlem2  32544  rmsuppfi  33166  mndpsuppfi  33168  scmsuppfi  33170  suppmptcfin  33172