Theorem oppcmon

Description: A monomorphism in the opposite category is an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	oppcmon.o	|- O = ( oppCat ` C )
	oppcmon.c	|- ( ph -> C e. Cat )
	oppcmon.m	|- M = ( Mono ` O )
	oppcmon.e	|- E = ( Epi ` C )
Assertion	oppcmon	|- ( ph -> ( X M Y ) = ( Y E X ) )

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	|- O = ( oppCat ` C )
2		oppcmon.c	|- ( ph -> C e. Cat )
3		oppcmon.m	|- M = ( Mono ` O )
4		oppcmon.e	|- E = ( Epi ` C )
5		fveq2	|- ( c = C -> ( oppCat ` c ) = ( oppCat ` C ) )
6	5 1	eqtr4di	|- ( c = C -> ( oppCat ` c ) = O )
7	6	fveq2d	|- ( c = C -> ( Mono ` ( oppCat ` c ) ) = ( Mono ` O ) )
8	7 3	eqtr4di	|- ( c = C -> ( Mono ` ( oppCat ` c ) ) = M )
9	8	tposeqd	|- ( c = C -> tpos ( Mono ` ( oppCat ` c ) ) = tpos M )
10		df-epi	|- Epi = ( c e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) )
11	3	fvexi	|- M e. _V
12	11	tposex	|- tpos M e. _V
13	9 10 12	fvmpt	|- ( C e. Cat -> ( Epi ` C ) = tpos M )
14	2 13	syl	|- ( ph -> ( Epi ` C ) = tpos M )
15	4 14	syl5eq	|- ( ph -> E = tpos M )
16	15	oveqd	|- ( ph -> ( Y E X ) = ( Y tpos M X ) )
17		ovtpos	|- ( Y tpos M X ) = ( X M Y )
18	16 17	eqtr2di	|- ( ph -> ( X M Y ) = ( Y E X ) )