Theorem ssfi 8065

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	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Proof of Theorem ssfi

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 7865	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		bren 7850	. . . . 5 ⊢ (𝐴 ≈ 𝑥 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝑥)
3		f1ofo 6057	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–onto→𝑥)
4		imassrn 5396	. . . . . . . . . . . 12 ⊢ (𝑧 “ 𝐵) ⊆ ran 𝑧
5		forn 6031	. . . . . . . . . . . 12 ⊢ (𝑧:𝐴–onto→𝑥 → ran 𝑧 = 𝑥)
6	4, 5	syl5sseq 3616	. . . . . . . . . . 11 ⊢ (𝑧:𝐴–onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
7	3, 6	syl 17	. . . . . . . . . 10 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → (𝑧 “ 𝐵) ⊆ 𝑥)
8		ssnnfi 8064	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → (𝑧 “ 𝐵) ∈ Fin)
9		isfi 7865	. . . . . . . . . . 11 ⊢ ((𝑧 “ 𝐵) ∈ Fin ↔ ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
10	8, 9	sylib 207	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ω ∧ (𝑧 “ 𝐵) ⊆ 𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
11	7, 10	sylan2 490	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑧:𝐴–1-1-onto→𝑥) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
12	11	adantrr 749	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → ∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦)
13		f1of1 6049	. . . . . . . . . . . . . 14 ⊢ (𝑧:𝐴–1-1-onto→𝑥 → 𝑧:𝐴–1-1→𝑥)
14		f1ores 6064	. . . . . . . . . . . . . 14 ⊢ ((𝑧:𝐴–1-1→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
15	13, 14	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵))
16		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑧 ∈ V
17	16	resex 5363	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ↾ 𝐵) ∈ V
18		f1oeq1 6040	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑧 ↾ 𝐵) → (𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵) ↔ (𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵)))
19	17, 18	spcev 3273	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
20		bren 7850	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≈ (𝑧 “ 𝐵) ↔ ∃𝑥 𝑥:𝐵–1-1-onto→(𝑧 “ 𝐵))
21	19, 20	sylibr 223	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) → 𝐵 ≈ (𝑧 “ 𝐵))
22		entr 7894	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ≈ (𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
23	21, 22	sylan 487	. . . . . . . . . . . . 13 ⊢ (((𝑧 ↾ 𝐵):𝐵–1-1-onto→(𝑧 “ 𝐵) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
24	15, 23	sylan 487	. . . . . . . . . . . 12 ⊢ (((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) ∧ (𝑧 “ 𝐵) ≈ 𝑦) → 𝐵 ≈ 𝑦)
25	24	ex 449	. . . . . . . . . . 11 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → ((𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ≈ 𝑦))
26	25	reximdv 2999	. . . . . . . . . 10 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → ∃𝑦 ∈ ω 𝐵 ≈ 𝑦))
27		isfi 7865	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin ↔ ∃𝑦 ∈ ω 𝐵 ≈ 𝑦)
28	26, 27	syl6ibr 241	. . . . . . . . 9 ⊢ ((𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
29	28	adantl 481	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → (∃𝑦 ∈ ω (𝑧 “ 𝐵) ≈ 𝑦 → 𝐵 ∈ Fin))
30	12, 29	mpd 15	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ (𝑧:𝐴–1-1-onto→𝑥 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ Fin)
31	30	exp32 629	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
32	31	exlimdv 1848	. . . . 5 ⊢ (𝑥 ∈ ω → (∃𝑧 𝑧:𝐴–1-1-onto→𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
33	2, 32	syl5bi 231	. . . 4 ⊢ (𝑥 ∈ ω → (𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin)))
34	33	rexlimiv 3009	. . 3 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
35	1, 34	sylbi 206	. 2 ⊢ (𝐴 ∈ Fin → (𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin))
36	35	imp 444	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897   ⊆ wss 3540   class class class wbr 4583  ran crn 5039   ↾ cres 5040   “ cima 5041  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ωcom 6957   ≈ cen 7838  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-om 6958  df-er 7629  df-en 7842  df-fin 7845

This theorem is referenced by:  domfi  8066  ssfid  8068  infi  8069  finresfin  8071  diffi  8077  findcard3  8088  unfir  8113  fnfi  8123  fofinf1o  8126  cnvfi  8131  f1fi  8136  imafi  8142  mapfi  8145  ixpfi  8146  ixpfi2  8147  mptfi  8148  cnvimamptfin  8150  fisuppfi  8166  suppssfifsupp  8173  fsuppunbi  8179  snopfsupp  8181  fsuppres  8183  ressuppfi  8184  fsuppmptif  8188  fsuppco2  8191  fsuppcor  8192  sniffsupp  8198  elfiun  8219  wemapso2lem  8340  cantnfp1lem1  8458  oemapvali  8464  ackbij2lem1  8924  ackbij1lem11  8935  fin23lem26  9030  fin23lem23  9031  fin23lem21  9044  fin11a  9088  isfin1-3  9091  axcclem  9162  ssnn0fi  12646  hashun3  13034  hashss  13058  hashssdif  13061  hashsslei  13073  hashbclem  13093  hashf1lem2  13097  seqcoll2  13106  pr2pwpr  13116  isercolllem2  14244  isercoll  14246  fsum2dlem  14343  fsumcom2OLD  14348  fsumless  14369  fsumabs  14374  fsumrlim  14384  fsumo1  14385  cvgcmpce  14391  fsumiun  14394  qshash  14398  incexclem  14407  incexc  14408  incexc2  14409  fprod2dlem  14549  fprodcom2OLD  14554  fprodmodd  14567  sumeven  14948  sumodd  14949  bitsfi  14997  bitsinv1  15002  bitsinvp1  15009  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  phicl2  15311  phibnd  15314  hashdvds  15318  phiprmpw  15319  phimullem  15322  eulerthlem2  15325  eulerth  15326  phisum  15333  sumhash  15438  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  1arith  15469  4sqlem11  15497  vdwlem11  15533  hashbccl  15545  ramlb  15561  0ram  15562  ramub1lem1  15568  ramub1lem2  15569  prmgaplem3  15595  prmgaplem4  15596  isstruct2  15704  lagsubg2  17478  lagsubg  17479  orbsta2  17570  symgbasfi  17629  symgfisg  17711  symggen2  17714  odcl2  17805  oddvds2  17806  sylow1lem2  17837  sylow1lem3  17838  sylow1lem4  17839  sylow1lem5  17840  odcau  17842  pgpssslw  17852  sylow2alem2  17856  sylow2a  17857  sylow2blem1  17858  sylow2blem3  17860  slwhash  17862  fislw  17863  sylow2  17864  sylow3lem1  17865  sylow3lem3  17867  sylow3lem4  17868  sylow3lem6  17870  cyggenod  18109  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzadd  18145  gsumpt  18184  gsum2dlem1  18192  gsum2dlem2  18193  gsum2d  18194  gsum2d2lem  18195  dprdfadd  18242  ablfacrplem  18287  ablfacrp2  18289  ablfac1c  18293  ablfac1eulem  18294  ablfac1eu  18295  pgpfac1lem5  18301  pgpfaclem2  18304  pgpfaclem3  18305  ablfaclem3  18309  lcomfsupp  18726  psrbaglecl  19190  psrbagaddcl  19191  psrbagcon  19192  mplsubg  19258  mpllss  19259  mplcoe5  19289  psrbagsn  19316  psr1baslem  19376  dsmmfi  19901  dsmmacl  19904  dsmmsubg  19906  dsmmlss  19907  frlmsslsp  19954  mamures  20015  submabas  20203  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  maducoeval2  20265  madugsum  20268  fctop  20618  restfpw  20793  fincmp  21006  cmpfi  21021  bwth  21023  finlocfin  21133  lfinpfin  21137  locfincmp  21139  1stckgenlem  21166  ptbasfi  21194  ptcnplem  21234  ptcmpfi  21426  cfinfil  21507  ufinffr  21543  fin1aufil  21546  tsmsres  21757  xrge0gsumle  22444  xrge0tsms  22445  fsumcn  22481  rrxcph  22988  rrxmval  22996  ovoliunlem1  23077  ovolicc2lem4  23095  ovolicc2lem5  23096  i1fima  23251  i1fd  23254  itg1cl  23258  itg1ge0  23259  i1f0  23260  i1f1  23263  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulc  23276  itg1mulc  23277  i1fres  23278  itg10a  23283  itg1ge0a  23284  itg1climres  23287  mbfi1fseqlem4  23291  itgfsum  23399  dvmptfsum  23542  plyexmo  23872  aannenlem2  23888  aalioulem2  23892  birthday  24481  jensenlem1  24513  jensenlem2  24514  jensen  24515  wilthlem2  24595  ppifi  24632  prmdvdsfi  24633  0sgm  24670  sgmf  24671  sgmnncl  24673  ppiprm  24677  chtprm  24679  chtdif  24684  efchtdvds  24685  ppidif  24689  ppiltx  24703  mumul  24707  sqff1o  24708  fsumdvdsdiag  24710  fsumdvdscom  24711  dvdsflsumcom  24714  musum  24717  musumsum  24718  muinv  24719  fsumdvdsmul  24721  ppiub  24729  vmasum  24741  logfac2  24742  perfectlem2  24755  dchrfi  24780  dchrabs  24785  dchrptlem1  24789  dchrptlem2  24790  dchrpt  24792  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  chebbnd1lem1  24958  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasumlem  24976  dchrvmasumlem1  24984  dchrisum0ff  24996  rpvmasum2  25001  dchrisum0re  25002  dchrisum0  25009  rplogsum  25016  dirith2  25017  vmalogdivsum2  25027  logsqvma  25031  logsqvma2  25032  selberg  25037  selberg34r  25060  pntsval2  25065  pntrlog2bndlem1  25066  cusgrafi  26010  wwlknfi  26266  hashwwlkext  26274  clwwlknfi  26306  qerclwwlknfi  26357  vdgrfiun  26429  eupath2lem3  26506  konigsberg  26514  relfi  28797  imafi2  28872  unifi3  28873  ffsrn  28892  gsumle  29110  xrge0tsmsd  29116  hasheuni  29474  carsgclctunlem1  29706  sibfof  29729  sitgclg  29731  oddpwdc  29743  eulerpartlems  29749  eulerpartlemb  29757  eulerpartlemmf  29764  eulerpartlemgf  29768  eulerpartlemgs2  29769  coinfliplem  29867  coinflippv  29872  ballotlemfelz  29879  ballotlemfp1  29880  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemiex  29890  ballotlemsup  29893  ballotlemfg  29914  ballotlemfrc  29915  ballotlemfrceq  29917  ballotth  29926  deranglem  30402  subfacp1lem3  30418  subfacp1lem5  30420  subfacp1lem6  30421  erdszelem2  30428  erdszelem8  30434  erdsze2lem2  30440  snmlff  30565  mvrsfpw  30657  finminlem  31482  topdifinffinlem  32371  matunitlindflem1  32575  poimirlem9  32588  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem30  32609  poimirlem32  32611  itg2addnclem2  32632  nnubfi  32716  nninfnub  32717  sstotbnd2  32743  cntotbnd  32765  rencldnfilem  36402  jm2.22  36580  jm2.23  36581  filnm  36678  pwssfi  38236  disjinfi  38375  fsumiunss  38642  fprodexp  38661  fprodabs2  38662  mccllem  38664  sumnnodd  38697  fprodcncf  38787  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  fourierdlem25  39025  fourierdlem37  39037  fourierdlem51  39050  fourierdlem79  39078  fouriersw  39124  etransclem16  39143  etransclem24  39151  etransclem33  39160  etransclem44  39171  sge0resplit  39299  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  carageniuncllem2  39412  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmvlelem4  39488  hoidmvlelem5  39489  fmtnoinf  39986  perfectALTVlem2  40165  cusgrfi  40674  wwlksnfi  41112  hashwwlksnext  41120  rmsuppfi  41948  mndpsuppfi  41950  scmsuppfi  41952  suppmptcfin  41954