Metamath Proof Explorer

Definition df-fsupp

Description: Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019)

Ref Expression
Assertion df-fsupp ${⊢}\mathrm{finSupp}=\left\{⟨{r},{z}⟩|\left(\mathrm{Fun}{r}\wedge {r}\mathrm{supp}{z}\in \mathrm{Fin}\right)\right\}$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfsupp ${class}\mathrm{finSupp}$
1 vr ${setvar}{r}$
2 vz ${setvar}{z}$
3 1 cv ${setvar}{r}$
4 3 wfun ${wff}\mathrm{Fun}{r}$
5 csupp ${class}\mathrm{supp}$
6 2 cv ${setvar}{z}$
7 3 6 5 co ${class}{supp}_{{z}}\left({r}\right)$
8 cfn ${class}\mathrm{Fin}$
9 7 8 wcel ${wff}{r}\mathrm{supp}{z}\in \mathrm{Fin}$
10 4 9 wa ${wff}\left(\mathrm{Fun}{r}\wedge {r}\mathrm{supp}{z}\in \mathrm{Fin}\right)$
11 10 1 2 copab ${class}\left\{⟨{r},{z}⟩|\left(\mathrm{Fun}{r}\wedge {r}\mathrm{supp}{z}\in \mathrm{Fin}\right)\right\}$
12 0 11 wceq ${wff}\mathrm{finSupp}=\left\{⟨{r},{z}⟩|\left(\mathrm{Fun}{r}\wedge {r}\mathrm{supp}{z}\in \mathrm{Fin}\right)\right\}$