Theorem fsuppimpd 9387

Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.)

Hypothesis

Ref	Expression
fsuppimpd.f	⊢ (𝜑 → 𝐹 finSupp 𝑍)

Assertion

Ref	Expression
fsuppimpd	⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Proof of Theorem fsuppimpd

Step	Hyp	Ref	Expression
1		fsuppimpd.f	. 2 ⊢ (𝜑 → 𝐹 finSupp 𝑍)
2		fsuppimp 9386	. . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin))
3	2	simprd 495	. 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin)
4	1, 3	syl 17	1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5142  Fun wfun 6536  (class class class)co 7414   supp csupp 8159  Fincfn 8957   finSupp cfsupp 9379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7417  df-fsupp 9380

This theorem is referenced by:  fsuppsssupp  9398  fsuppsssuppgd  9399  fsuppxpfi  9402  fsuppun  9404  resfsupp  9413  fsuppmptif  9416  fsuppco  9419  fsuppco2  9420  fsuppcor  9421  cantnfcl  9684  cantnfp1lem1  9695  fsuppmapnn0fiublem  13981  fsuppmapnn0fiub  13982  fsuppmapnn0ub  13986  gsumzcl  19859  gsumcl  19863  gsumzadd  19870  gsumzmhm  19885  gsumzoppg  19892  gsum2dlem1  19918  gsum2dlem2  19919  gsum2d  19920  gsumxp2  19928  gsumdixp  20248  lcomfsupp  20778  mptscmfsupp0  20803  regsumsupp  21547  frlmphllem  21707  uvcresum  21720  frlmsslsp  21723  frlmup1  21725  mplcoe1  21968  mplbas2  21973  psrbagev1  22014  psrbagev1OLD  22015  evlslem2  22018  evlslem6  22020  psdmplcl  22079  tsmsgsum  24036  rrxcph  25313  rrxfsupp  25323  mdegldg  25995  mdegcl  25998  plypf1  26139  fsuppinisegfi  32461  fsupprnfi  32466  fsuppcurry1  32501  fsuppcurry2  32502  offinsupp1  32503  gsumhashmul  32764  rmfsupp2  32940  elrspunidl  33138  elrspunsn  33139  evls1fpws  33240  fedgmullem1  33317  fedgmullem2  33318  evls1fldgencl  33348  zarcmplem  33476  fsuppind  41817  mnringmulrcld  43659  rmfsupp  47432  mndpfsupp  47434  scmfsupp  47436  lincresunit2  47540

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »