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

Definition df-fsupp 7624
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 7623 . 2  class finSupp
2 vr . . . . . 6  setvar  r
32cv 1368 . . . . 5  class  r
43wfun 5415 . . . 4  wff  Fun  r
5 vz . . . . . . 7  setvar  z
65cv 1368 . . . . . 6  class  z
7 csupp 6693 . . . . . 6  class supp
83, 6, 7co 6094 . . . . 5  class  ( r supp  z )
9 cfn 7313 . . . . 5  class  Fin
108, 9wcel 1756 . . . 4  wff  ( r supp  z )  e.  Fin
114, 10wa 369 . . 3  wff  ( Fun  r  /\  ( r supp  z )  e.  Fin )
1211, 2, 5copab 4352 . 2  class  { <. r ,  z >.  |  ( Fun  r  /\  (
r supp  z )  e. 
Fin ) }
131, 12wceq 1369 1  wff finSupp  =  { <. r ,  z >.  |  ( Fun  r  /\  ( r supp  z )  e.  Fin ) }
Colors of variables: wff setvar class
This definition is referenced by:  relfsupp  7625  isfsupp  7627  fsuppimp  7629  wemapso2  7771
  Copyright terms: Public domain W3C validator