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

Definition df-funpart 31150
Description: Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 31220 and funpartfv 31222 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.)
Assertion
Ref Expression
df-funpart Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))

Detailed syntax breakdown of Definition df-funpart
StepHypRef Expression
1 cF . . 3 class 𝐹
21cfunpart 31125 . 2 class Funpart𝐹
31cimage 31116 . . . . . 6 class Image𝐹
4 csingle 31114 . . . . . 6 class Singleton
53, 4ccom 5042 . . . . 5 class (Image𝐹 ∘ Singleton)
6 cvv 3173 . . . . . 6 class V
7 csingles 31115 . . . . . 6 class Singletons
86, 7cxp 5036 . . . . 5 class (V × Singletons )
95, 8cin 3539 . . . 4 class ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))
109cdm 5038 . . 3 class dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))
111, 10cres 5040 . 2 class (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
122, 11wceq 1475 1 wff Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )))
Colors of variables: wff setvar class
This definition is referenced by:  funpartfun  31220  funpartss  31221  funpartfv  31222
  Copyright terms: Public domain W3C validator