This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in 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 \in Cat ⟼ tpos Mono (oppCat (c)))$
10	0 9	wceq	$wff Epi = (c \in Cat ⟼ tpos Mono (oppCat (c)))$