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 e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cepi 
 |-  Epi
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 cmon 
 |-  Mono
4 coppc 
 |-  oppCat
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( oppCat ` c )
7 6 3 cfv 
 |-  ( Mono ` ( oppCat ` c ) )
8 7 ctpos 
 |-  tpos ( Mono ` ( oppCat ` c ) )
9 1 2 8 cmpt 
 |-  ( c e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) )
10 0 9 wceq 
 |-  Epi = ( c e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) )