![]() |
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 9399 | . . 3 ⊢ (𝐹 finSupp 𝑍 → (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin)) | |
3 | 2 | simprd 494 | . 2 ⊢ (𝐹 finSupp 𝑍 → (𝐹 supp 𝑍) ∈ Fin) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 class class class wbr 5149 Fun wfun 6543 (class class class)co 7419 supp csupp 8165 Fincfn 8964 finSupp cfsupp 9392 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-iota 6501 df-fun 6551 df-fv 6557 df-ov 7422 df-fsupp 9393 |
This theorem is referenced by: fsuppsssupp 9411 fsuppsssuppgd 9412 fsuppxpfi 9415 fsuppun 9417 resfsupp 9426 fsuppmptif 9429 fsuppco 9432 fsuppco2 9433 fsuppcor 9434 cantnfcl 9697 cantnfp1lem1 9708 fsuppmapnn0fiublem 13996 fsuppmapnn0fiub 13997 fsuppmapnn0ub 14001 gsumzcl 19883 gsumcl 19887 gsumzadd 19894 gsumzmhm 19909 gsumzoppg 19916 gsum2dlem1 19942 gsum2dlem2 19943 gsum2d 19944 gsumxp2 19952 gsumdixp 20272 lcomfsupp 20802 mptscmfsupp0 20827 regsumsupp 21576 frlmphllem 21736 uvcresum 21749 frlmsslsp 21752 frlmup1 21754 mplcoe1 22002 mplbas2 22007 psrbagev1 22048 psrbagev1OLD 22049 evlslem2 22052 evlslem6 22054 psdmplcl 22114 evls1fpws 22318 tsmsgsum 24092 rrxcph 25369 rrxfsupp 25379 mdegldg 26051 mdegcl 26054 plypf1 26196 fsuppinisegfi 32554 fsupprnfi 32559 fsuppcurry1 32594 fsuppcurry2 32595 offinsupp1 32596 gsumhashmul 32865 rmfsupp2 33043 elrspunidl 33245 elrspunsn 33246 rprmdvdsprod 33351 fedgmullem1 33460 fedgmullem2 33461 evls1fldgencl 33491 zarcmplem 33615 fsuppind 41960 mnringmulrcld 43809 rmfsupp 47626 mndpfsupp 47628 scmfsupp 47630 lincresunit2 47734 |
Copyright terms: Public domain | W3C validator |