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 F = ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | |- F |
|
| 1 | 0 | cfunpart | |- Funpart F |
| 2 | 0 | cimage | |- Image F |
| 3 | csingle | |- Singleton |
|
| 4 | 2 3 | ccom | |- ( Image F o. Singleton ) |
| 5 | cvv | |- _V |
|
| 6 | csingles | |- Singletons |
|
| 7 | 5 6 | cxp | |- ( _V X. Singletons ) |
| 8 | 4 7 | cin | |- ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) |
| 9 | 8 | cdm | |- dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) |
| 10 | 0 9 | cres | |- ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) |
| 11 | 1 10 | wceq | |- Funpart F = ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) |