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	$$⊢\mathrm{Epi}=\left(c\in \mathrm{Cat}⟼tpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cepi	$$class\mathrm{Epi}$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		cmon	$$class\mathrm{Mono}$$
4		coppc	$$class\mathrm{oppCat}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class\mathrm{oppCat}\left(c\right)$$
7	6 3	cfv	$$class\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)$$
8	7	ctpos	$$classtpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)$$
9	1 2 8	cmpt	$$class\left(c\in \mathrm{Cat}⟼tpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)\right)$$
10	0 9	wceq	$$wff\mathrm{Epi}=\left(c\in \mathrm{Cat}⟼tpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)\right)$$