MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fsupp Structured version   Unicode version

Definition df-fsupp 7890
Description: Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.)
Assertion
Ref Expression
df-fsupp  |- finSupp  =  { <. r ,  z >.  |  ( Fun  r  /\  ( r supp  z )  e.  Fin ) }
Distinct variable group:    z, r

Detailed syntax breakdown of Definition df-fsupp
StepHypRef Expression
1 cfsupp 7889 . 2  class finSupp
2 vr . . . . . 6  setvar  r
32cv 1436 . . . . 5  class  r
43wfun 5595 . . . 4  wff  Fun  r
5 vz . . . . . . 7  setvar  z
65cv 1436 . . . . . 6  class  z
7 csupp 6925 . . . . . 6  class supp
83, 6, 7co 6305 . . . . 5  class  ( r supp  z )
9 cfn 7577 . . . . 5  class  Fin
108, 9wcel 1870 . . . 4  wff  ( r supp  z )  e.  Fin
114, 10wa 370 . . 3  wff  ( Fun  r  /\  ( r supp  z )  e.  Fin )
1211, 2, 5copab 4483 . 2  class  { <. r ,  z >.  |  ( Fun  r  /\  (
r supp  z )  e. 
Fin ) }
131, 12wceq 1437 1  wff finSupp  =  { <. r ,  z >.  |  ( Fun  r  /\  ( r supp  z )  e.  Fin ) }
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  7891  isfsupp  7893
  Copyright terms: Public domain W3C validator