Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-funpart Unicode version

Definition df-funpart 24486
Description: Define the functional part of a class  F. This is the maximal part of  F that is a function. See funpartfun 24553 and funpartfv 24555 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
Assertion
Ref Expression
df-funpart  |- Funpart F  =  ( F  |`  dom  (
(Image F  o. Singleton )  i^i  ( _V  X.  Singletons ) ) )

Detailed syntax breakdown of Definition df-funpart
StepHypRef Expression
1 cF . . 3  class  F
21cfunpart 24463 . 2  class Funpart F
31cimage 24454 . . . . . 6  class Image F
4 csingle 24452 . . . . . 6  class Singleton
53, 4ccom 4709 . . . . 5  class  (Image F  o. Singleton )
6 cvv 2801 . . . . . 6  class  _V
7 csingles 24453 . . . . . 6  class  Singletons
86, 7cxp 4703 . . . . 5  class  ( _V 
X.  Singletons )
95, 8cin 3164 . . . 4  class  ( (Image
F  o. Singleton )  i^i  ( _V  X.  Singletons ) )
109cdm 4705 . . 3  class  dom  (
(Image F  o. Singleton )  i^i  ( _V  X.  Singletons ) )
111, 10cres 4707 . 2  class  ( F  |`  dom  ( (Image F  o. Singleton )  i^i  ( _V 
X.  Singletons ) ) )
122, 11wceq 1632 1  wff Funpart F  =  ( F  |`  dom  (
(Image F  o. Singleton )  i^i  ( _V  X.  Singletons ) ) )
Colors of variables: wff set class
This definition is referenced by:  funpartfun  24553  funpartss  24554  funpartfv  24555
  Copyright terms: Public domain W3C validator