![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isfsupp | Structured version Visualization version GIF version |
Description: The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
Ref | Expression |
---|---|
isfsupp | ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funeq 6250 | . . . 4 ⊢ (𝑟 = 𝑅 → (Fun 𝑟 ↔ Fun 𝑅)) | |
2 | 1 | adantr 481 | . . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → (Fun 𝑟 ↔ Fun 𝑅)) |
3 | oveq12 7030 | . . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → (𝑟 supp 𝑧) = (𝑅 supp 𝑍)) | |
4 | 3 | eleq1d 2867 | . . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → ((𝑟 supp 𝑧) ∈ Fin ↔ (𝑅 supp 𝑍) ∈ Fin)) |
5 | 2, 4 | anbi12d 630 | . 2 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → ((Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin))) |
6 | df-fsupp 8685 | . 2 ⊢ finSupp = {〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} | |
7 | 5, 6 | brabga 5316 | 1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 class class class wbr 4966 Fun wfun 6224 (class class class)co 7021 supp csupp 7686 Fincfn 8362 finSupp cfsupp 8684 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pr 5226 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-rel 5455 df-cnv 5456 df-co 5457 df-iota 6194 df-fun 6232 df-fv 6238 df-ov 7024 df-fsupp 8685 |
This theorem is referenced by: funisfsupp 8689 fsuppimp 8690 fdmfifsupp 8694 fczfsuppd 8702 fsuppmptif 8714 fsuppco2 8717 fsuppcor 8718 gsumzadd 18767 gsumpt 18807 gsum2dlem2 18816 gsum2d 18817 gsum2d2lem 18818 rmfsupp2 30525 rmfsupp 43928 mndpfsupp 43930 scmfsupp 43932 mptcfsupp 43934 |
Copyright terms: Public domain | W3C validator |