Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fsuppimpd | Structured version Visualization version GIF version |
Description: A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.) |
Ref | Expression |
---|---|
fsuppimpd.f | ⊢ (𝜑 → 𝐹 finSupp 𝑍) |
Ref | Expression |
---|---|
fsuppimpd | ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsuppimpd.f | . 2 ⊢ (𝜑 → 𝐹 finSupp 𝑍) | |
2 | fsuppimp 8905 | . . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin)) | |
3 | 2 | simprd 499 | . 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 class class class wbr 5027 Fun wfun 6327 (class class class)co 7164 supp csupp 7849 Fincfn 8548 finSupp cfsupp 8899 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3399 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-iota 6291 df-fun 6335 df-fv 6341 df-ov 7167 df-fsupp 8900 |
This theorem is referenced by: fsuppsssupp 8915 fsuppxpfi 8916 fsuppun 8918 resfsupp 8926 fsuppmptif 8929 fsuppco 8932 fsuppco2 8933 fsuppcor 8934 cantnfcl 9196 cantnfp1lem1 9207 fsuppmapnn0fiublem 13442 fsuppmapnn0fiub 13443 fsuppmapnn0ub 13447 gsumzcl 19143 gsumcl 19147 gsumzadd 19154 gsumzmhm 19169 gsumzoppg 19176 gsum2dlem1 19202 gsum2dlem2 19203 gsum2d 19204 gsumxp2 19212 gsumdixp 19474 lcomfsupp 19786 mptscmfsupp0 19811 regsumsupp 20431 frlmphllem 20589 uvcresum 20602 frlmsslsp 20605 frlmup1 20607 mplcoe1 20841 mplbas2 20846 psrbagev1 20882 psrbagev1OLD 20883 evlslem2 20886 evlslem6 20888 tsmsgsum 22883 rrxcph 24137 rrxfsupp 24147 mdegldg 24811 mdegcl 24814 plypf1 24953 fsuppinisegfi 30588 fsupprnfi 30593 fsuppcurry1 30627 fsuppcurry2 30628 offinsupp1 30629 gsumhashmul 30885 rmfsupp2 31061 elrspunidl 31170 fedgmullem1 31274 fedgmullem2 31275 zarcmplem 31395 evlsbagval 39838 fsuppind 39842 mhphf 39848 mnringmulrcld 41372 rmfsupp 45228 mndpfsupp 45230 scmfsupp 45232 lincresunit2 45337 |
Copyright terms: Public domain | W3C validator |