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