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