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

Definition df-funpart 24415
Description: Define the functional part of a class  F. This is the maximal part of  F that is a function. See funpartfun 24481 and funpartfv 24483 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 24392 . 2  class Funpart F
31cimage 24383 . . . . . 6  class Image F
4 csingle 24381 . . . . . 6  class Singleton
53, 4ccom 4693 . . . . 5  class  (Image F  o. Singleton )
6 cvv 2788 . . . . . 6  class  _V
7 csingles 24382 . . . . . 6  class  Singletons
86, 7cxp 4687 . . . . 5  class  ( _V 
X.  Singletons )
95, 8cin 3151 . . . 4  class  ( (Image
F  o. Singleton )  i^i  ( _V  X.  Singletons ) )
109cdm 4689 . . 3  class  dom  (
(Image F  o. Singleton )  i^i  ( _V  X.  Singletons ) )
111, 10cres 4691 . 2  class  ( F  |`  dom  ( (Image F  o. Singleton )  i^i  ( _V 
X.  Singletons ) ) )
122, 11wceq 1623 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  24481  funpartss  24482  funpartfv  24483
  Copyright terms: Public domain W3C validator