Theorem oppcepi

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

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

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	|- O = ( oppCat ` C )
2		oppcmon.c	|- ( ph -> C e. Cat )
3		oppcepi.e	|- E = ( Epi ` O )
4		oppcepi.m	|- M = ( Mono ` C )
5	1	2oppchomf	|- ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
6	5	a1i	|- ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
7	1	2oppccomf	|- ( comf ` C ) = ( comf ` ( oppCat ` O ) )
8	7	a1i	|- ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
9	1	oppccat	|- ( C e. Cat -> O e. Cat )
10	2 9	syl	|- ( ph -> O e. Cat )
11		eqid	|- ( oppCat ` O ) = ( oppCat ` O )
12	11	oppccat	|- ( O e. Cat -> ( oppCat ` O ) e. Cat )
13	10 12	syl	|- ( ph -> ( oppCat ` O ) e. Cat )
14	6 8 2 13	monpropd	|- ( ph -> ( Mono ` C ) = ( Mono ` ( oppCat ` O ) ) )
15	4 14	syl5eq	|- ( ph -> M = ( Mono ` ( oppCat ` O ) ) )
16	15	oveqd	|- ( ph -> ( Y M X ) = ( Y ( Mono ` ( oppCat ` O ) ) X ) )
17		eqid	|- ( Mono ` ( oppCat ` O ) ) = ( Mono ` ( oppCat ` O ) )
18	11 10 17 3	oppcmon	|- ( ph -> ( Y ( Mono ` ( oppCat ` O ) ) X ) = ( X E Y ) )
19	16 18	eqtr2d	|- ( ph -> ( X E Y ) = ( Y M X ) )