Metamath Proof Explorer


Definition df-epi

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 Epi = c Cat tpos Mono oppCat c

Detailed syntax breakdown

Step Hyp Ref Expression
0 cepi class Epi
1 vc setvar c
2 ccat class Cat
3 cmon class Mono
4 coppc class oppCat
5 1 cv setvar c
6 5 4 cfv class oppCat c
7 6 3 cfv class Mono oppCat c
8 7 ctpos class tpos Mono oppCat c
9 1 2 8 cmpt class c Cat tpos Mono oppCat c
10 0 9 wceq wff Epi = c Cat tpos Mono oppCat c