Description: Function returning the epimorphisms of the category c . JFM CAT_1 def. 11. (Contributed by FL, 8-Aug-2008) (Revised by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | df-epi |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cepi | ||
1 | vc | ||
2 | ccat | ||
3 | cmon | ||
4 | coppc | ||
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | 6 3 | cfv | |
8 | 7 | ctpos | |
9 | 1 2 8 | cmpt | |
10 | 0 9 | wceq |