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 = ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cepi	⊢ Epi
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		cmon	⊢ Mono
4		coppc	⊢ oppCat
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( oppCat ‘ 𝑐 )
7	6 3	cfv	⊢ ( Mono ‘ ( oppCat ‘ 𝑐 ) )
8	7	ctpos	⊢ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) )
9	1 2 8	cmpt	⊢ ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )
10	0 9	wceq	⊢ Epi = ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )