Metamath Proof Explorer


Definition df-funpart

Description: Define the functional part of a class F . This is the maximal part of F that is a function. See funpartfun and funpartfv for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014)

Ref Expression
Assertion df-funpart Funpart 𝐹 = ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF 𝐹
1 0 cfunpart Funpart 𝐹
2 0 cimage Image 𝐹
3 csingle Singleton
4 2 3 ccom ( Image 𝐹 ∘ Singleton )
5 cvv V
6 csingles Singletons
7 5 6 cxp ( V × Singletons )
8 4 7 cin ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) )
9 8 cdm dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) )
10 0 9 cres ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )
11 1 10 wceq Funpart 𝐹 = ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )