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 9134 | . . 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 2106 class class class wbr 5074 Fun wfun 6427 (class class class)co 7275 supp csupp 7977 Fincfn 8733 finSupp cfsupp 9128 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-iota 6391 df-fun 6435 df-fv 6441 df-ov 7278 df-fsupp 9129 |
This theorem is referenced by: fsuppsssupp 9144 fsuppxpfi 9145 fsuppun 9147 resfsupp 9155 fsuppmptif 9158 fsuppco 9161 fsuppco2 9162 fsuppcor 9163 cantnfcl 9425 cantnfp1lem1 9436 fsuppmapnn0fiublem 13710 fsuppmapnn0fiub 13711 fsuppmapnn0ub 13715 gsumzcl 19512 gsumcl 19516 gsumzadd 19523 gsumzmhm 19538 gsumzoppg 19545 gsum2dlem1 19571 gsum2dlem2 19572 gsum2d 19573 gsumxp2 19581 gsumdixp 19848 lcomfsupp 20163 mptscmfsupp0 20188 regsumsupp 20827 frlmphllem 20987 uvcresum 21000 frlmsslsp 21003 frlmup1 21005 mplcoe1 21238 mplbas2 21243 psrbagev1 21285 psrbagev1OLD 21286 evlslem2 21289 evlslem6 21291 tsmsgsum 23290 rrxcph 24556 rrxfsupp 24566 mdegldg 25231 mdegcl 25234 plypf1 25373 fsuppinisegfi 31021 fsupprnfi 31026 fsuppcurry1 31060 fsuppcurry2 31061 offinsupp1 31062 gsumhashmul 31316 rmfsupp2 31492 elrspunidl 31606 fedgmullem1 31710 fedgmullem2 31711 zarcmplem 31831 evlsbagval 40275 fsuppind 40279 mhphf 40285 mnringmulrcld 41846 rmfsupp 45710 mndpfsupp 45712 scmfsupp 45714 lincresunit2 45819 |
Copyright terms: Public domain | W3C validator |