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 8827 | . . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin)) | |
3 | 2 | simprd 496 | . 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 class class class wbr 5057 Fun wfun 6342 (class class class)co 7145 supp csupp 7819 Fincfn 8497 finSupp cfsupp 8821 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-iota 6307 df-fun 6350 df-fv 6356 df-ov 7148 df-fsupp 8822 |
This theorem is referenced by: fsuppsssupp 8837 fsuppxpfi 8838 fsuppun 8840 resfsupp 8848 fsuppmptif 8851 fsuppco 8853 fsuppco2 8854 fsuppcor 8855 cantnfcl 9118 cantnfp1lem1 9129 fsuppmapnn0fiublem 13346 fsuppmapnn0fiub 13347 fsuppmapnn0ub 13351 gsumzcl 18960 gsumcl 18964 gsumzadd 18971 gsumzmhm 18986 gsumzoppg 18993 gsum2dlem1 19019 gsum2dlem2 19020 gsum2d 19021 gsumxp2 19029 gsumdixp 19288 lcomfsupp 19603 mptscmfsupp0 19628 mplcoe1 20174 mplbas2 20179 psrbagev1 20218 evlslem2 20220 evlslem6 20222 regsumsupp 20694 frlmphllem 20852 uvcresum 20865 frlmsslsp 20868 frlmup1 20870 tsmsgsum 22674 rrxcph 23922 rrxfsupp 23932 mdegldg 24587 mdegcl 24590 plypf1 24729 fsuppcurry1 30387 fsuppcurry2 30388 offinsupp1 30389 rmfsupp2 30793 fedgmullem1 30924 fedgmullem2 30925 rmfsupp 44350 mndpfsupp 44352 scmfsupp 44354 lincresunit2 44461 |
Copyright terms: Public domain | W3C validator |