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 ) ) ) |
| 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 ) ) ) |