Theorem ssfi 7288

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 7090	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		bren 7076	. . . . 5 |- ( A ~~ x <-> E. z z : A -1-1-onto-> x )
3		f1ofo 5640	. . . . . . . . . . 11 |- ( z : A -1-1-onto-> x -> z : A -onto-> x )
4		imassrn 5175	. . . . . . . . . . . 12 |- ( z " B ) C_ ran z
5		forn 5615	. . . . . . . . . . . 12 |- ( z : A -onto-> x -> ran z = x )
6	4, 5	syl5sseq 3356	. . . . . . . . . . 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 7287	. . . . . . . . . . 11 |- ( ( x e. om /\ ( z " B ) C_ x ) -> ( z " B ) e. Fin )
9		isfi 7090	. . . . . . . . . . 11 |- ( ( z " B ) e. Fin <-> E. y e. om ( z " B ) ~~ y )
10	8, 9	sylib 189	. . . . . . . . . 10 |- ( ( x e. om /\ ( z " B ) C_ x ) -> E. y e. om ( z " B ) ~~ y )
11	7, 10	sylan2 461	. . . . . . . . 9 |- ( ( x e. om /\ z : A -1-1-onto-> x ) -> E. y e. om ( z " B ) ~~ y )
12	11	adantrr 698	. . . . . . . 8 |- ( ( x e. om /\ ( z : A -1-1-onto-> x /\ B C_ A ) ) -> E. y e. om ( z " B ) ~~ y )
13		f1of1 5632	. . . . . . . . . . . . . 14 |- ( z : A -1-1-onto-> x -> z : A -1-1-> x )
14		f1ores 5648	. . . . . . . . . . . . . 14 |- ( ( z : A -1-1-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
15	13, 14	sylan 458	. . . . . . . . . . . . 13 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( z |` B ) : B -1-1-onto-> ( z " B ) )
16		vex 2919	. . . . . . . . . . . . . . . . 17 |- z e. _V
17	16	resex 5145	. . . . . . . . . . . . . . . 16 |- ( z |` B ) e. _V
18		f1oeq1 5624	. . . . . . . . . . . . . . . 16 |- ( x = ( z |` B ) -> ( x : B -1-1-onto-> ( z " B ) <-> ( z |` B ) : B -1-1-onto-> ( z " B ) ) )
19	17, 18	spcev 3003	. . . . . . . . . . . . . . 15 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> E. x x : B -1-1-onto-> ( z " B ) )
20		bren 7076	. . . . . . . . . . . . . . 15 |- ( B ~~ ( z " B ) <-> E. x x : B -1-1-onto-> ( z " B ) )
21	19, 20	sylibr 204	. . . . . . . . . . . . . 14 |- ( ( z |` B ) : B -1-1-onto-> ( z " B ) -> B ~~ ( z " B ) )
22		entr 7118	. . . . . . . . . . . . . 14 |- ( ( B ~~ ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
23	21, 22	sylan 458	. . . . . . . . . . . . 13 |- ( ( ( z |` B ) : B -1-1-onto-> ( z " B ) /\ ( z " B ) ~~ y ) -> B ~~ y )
24	15, 23	sylan 458	. . . . . . . . . . . 12 |- ( ( ( z : A -1-1-onto-> x /\ B C_ A ) /\ ( z " B ) ~~ y ) -> B ~~ y )
25	24	ex 424	. . . . . . . . . . 11 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( ( z " B ) ~~ y -> B ~~ y ) )
26	25	reximdv 2777	. . . . . . . . . 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 7090	. . . . . . . . . 10 |- ( B e. Fin <-> E. y e. om B ~~ y )
28	26, 27	syl6ibr 219	. . . . . . . . 9 |- ( ( z : A -1-1-onto-> x /\ B C_ A ) -> ( E. y e. om ( z " B ) ~~ y -> B e. Fin ) )
29	28	adantl 453	. . . . . . . 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 589	. . . . . 6 |- ( x e. om -> ( z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
32	31	exlimdv 1643	. . . . 5 |- ( x e. om -> ( E. z z : A -1-1-onto-> x -> ( B C_ A -> B e. Fin ) ) )
33	2, 32	syl5bi 209	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C_ A -> B e. Fin ) ) )
34	33	rexlimiv 2784	. . 3 |- ( E. x e. om A ~~ x -> ( B C_ A -> B e. Fin ) )
35	1, 34	sylbi 188	. 2 |- ( A e. Fin -> ( B C_ A -> B e. Fin ) )
36	35	imp 419	1 |- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )

Syntax hints:   -> wi 4   /\ wa 359   E.wex 1547   e. wcel 1721   E.wrex 2667   C_ wss 3280   class class class wbr 4172   omcom 4804   ran crn 4838   |` cres 4839   "cima 4840   -1-1->wf1 5410   -onto->wfo 5411   -1-1-onto->wf1o 5412   ~~ cen 7065   Fincfn 7068

This theorem is referenced by:  domfi  7289  infi  7291  finresfin  7293  diffi  7298  findcard3  7309  unfir  7334  fnfi  7343  fofinf1o  7346  cnvfi  7349  f1fi  7352  imafi  7357  mapfi  7361  ixpfi  7362  ixpfi2  7363  mptfi  7364  elfiun  7393  marypha1lem  7396  wemapso2  7477  cantnfp1lem1  7590  oemapvali  7596  cantnflem1d  7600  cantnflem1  7601  mapfien  7609  ackbij2lem1  8055  ackbij1lem11  8066  fin23lem26  8161  fin23lem23  8162  fin23lem21  8175  fin11a  8219  isfin1-3  8222  axcclem  8293  pwfseqlem4  8493  hashun3  11613  hashssdif  11632  hashsslei  11640  hashbclem  11656  hashf1lem2  11660  seqcoll2  11668  isercolllem2  12414  isercoll  12416  fsumss  12474  fsum2dlem  12509  fsumcom2  12513  fsumless  12530  fsumabs  12535  fsumrlim  12545  fsumo1  12546  cvgcmpce  12552  fsumiun  12555  qshash  12561  incexclem  12571  incexc  12572  incexc2  12573  bitsfi  12904  bitsinv1  12909  bitsinvp1  12916  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  phicl2  13112  phibnd  13115  hashdvds  13119  phiprmpw  13120  phimullem  13123  eulerthlem2  13126  eulerth  13127  sumhash  13220  prmreclem2  13240  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  1arith  13250  4sqlem11  13278  vdwlem11  13314  hashbccl  13326  ramlb  13342  0ram  13343  ramub1lem1  13349  ramub1lem2  13350  isstruct2  13433  fisuppfi  14728  lagsubg2  14956  lagsubg  14957  orbsta2  15046  odcl2  15156  oddvds2  15157  sylow1lem2  15188  sylow1lem3  15189  sylow1lem4  15190  sylow1lem5  15191  odcau  15193  pgpssslw  15203  sylow2alem2  15207  sylow2a  15208  sylow2blem1  15209  sylow2blem3  15211  slwhash  15213  fislw  15214  sylow2  15215  sylow3lem1  15216  sylow3lem3  15218  sylow3lem4  15219  sylow3lem6  15221  cyggenod  15449  gsumval3  15469  gsumzadd  15482  gsumzsplit  15484  gsumzinv  15495  gsumsub  15497  gsumunsn  15499  gsumpt  15500  gsum2d  15501  gsum2d2lem  15502  dprdfid  15530  dprdfinv  15532  dprdfadd  15533  dprdsubg  15537  dmdprdsplitlem  15550  dpjidcl  15571  ablfacrplem  15578  ablfacrp2  15580  ablfac1c  15584  ablfac1eulem  15585  ablfac1eu  15586  pgpfac1lem5  15592  pgpfaclem2  15595  pgpfaclem3  15596  ablfaclem3  15600  psrbaglecl  16389  psrbagaddcl  16390  psrbagcon  16391  psrass1lem  16397  psrbas  16398  psrlidm  16422  psrridm  16423  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  psrass23  16428  mvridlem  16438  mplsubg  16455  mpllss  16456  mplsubrglem  16457  mplsubrg  16458  mvrcl  16467  mplmon  16481  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  mplbas2  16486  psrbagsn  16510  psrbagev1  16521  evlslem2  16523  psr1baslem  16538  psropprmul  16587  coe1mul2  16617  ply1coe  16639  fctop  17023  restfpw  17197  fincmp  17410  cmpfi  17425  1stckgenlem  17538  ptbasfi  17566  ptcnplem  17606  ptcmpfi  17798  cfinfil  17878  ufinffr  17914  fin1aufil  17917  tsms0  18124  tsmsres  18126  tgptsmscls  18132  xrge0gsumle  18817  xrge0tsms  18818  fsumcn  18853  ovoliunlem1  19351  ovolicc2lem4  19369  ovolicc2lem5  19370  i1fima  19523  i1fd  19526  itg1cl  19530  itg1ge0  19531  i1f0  19532  i1f1  19535  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulc  19548  itg1mulc  19549  i1fres  19550  itg10a  19555  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem4  19563  itgfsum  19671  dvmptfsum  19812  evlslem6  19887  evlslem3  19888  tdeglem4  19936  plypf1  20084  plyexmo  20183  aannenlem2  20199  aalioulem2  20203  tayl0  20231  birthday  20746  jensenlem1  20778  jensenlem2  20779  jensen  20780  wilthlem2  20805  ppifi  20841  prmdvdsfi  20843  0sgm  20880  sgmf  20881  sgmnncl  20883  ppiprm  20887  chtprm  20889  chtdif  20894  efchtdvds  20895  ppidif  20899  ppiltx  20913  mumul  20917  sqff1o  20918  fsumdvdsdiag  20922  fsumdvdscom  20923  dvdsflsumcom  20926  musum  20929  musumsum  20930  muinv  20931  fsumdvdsmul  20933  ppiub  20941  vmasum  20953  logfac2  20954  perfectlem2  20967  dchrfi  20992  dchrabs  20997  dchrptlem1  21001  dchrptlem2  21002  dchrptlem3  21003  dchrpt  21004  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  chebbnd1lem1  21116  chtppilimlem1  21120  rplogsumlem2  21132  rpvmasumlem  21134  dchrvmasumlem1  21142  dchrisum0ff  21154  rpvmasum2  21159  dchrisum0re  21160  dchrisum0  21167  rplogsum  21174  dirith2  21175  vmalogdivsum2  21185  logsqvma  21189  logsqvma2  21190  selberg  21195  selberg34r  21218  pntsval2  21223  pntrlog2bndlem1  21224  cusgrafi  21444  vdgrfiun  21626  eupath2lem3  21654  konigsberg  21662  xrge0tsmsd  24176  hasheuni  24428  sibfof  24607  sitgclg  24609  coinfliplem  24689  coinflippv  24694  ballotlemfelz  24701  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemiex  24712  ballotlemsup  24715  ballotlemfg  24736  ballotlemfrc  24737  ballotlemfrceq  24739  ballotth  24748  deranglem  24805  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  erdszelem2  24831  erdszelem8  24837  erdsze2lem2  24843  snmlff  24969  fprod2dlem  25257  fprodcom2  25261  itg2addnclem2  26156  finminlem  26211  finlocfin  26269  lfinpfin  26273  locfincmp  26274  nnubfi  26344  nninfnub  26345  sstotbnd2  26373  cntotbnd  26395  funsnfsup  26633  lcomfsup  26637  rencldnfilem  26771  jm2.22  26956  jm2.23  26957  filnm  27060  dsmmfi  27072  dsmmacl  27075  dsmmsubg  27077  dsmmlss  27078  uvcff  27108  uvcresum  27110  frlmsplit2  27111  frlmsslsp  27116  frlmup1  27118  symgfisg  27277  symggen2  27280  psgnghm2  27306  phisum  27386

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-er 6864  df-en 7069  df-fin 7072