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=\mathrm{oppCat}\left(C\right)$$
	oppcmon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppcepi.e	$$⊢E=\mathrm{Epi}\left(O\right)$$
	oppcepi.m	$$⊢M=\mathrm{Mono}\left(C\right)$$
Assertion	oppcepi	$$⊢\phi \to XEY=YMX$$

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcmon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		oppcepi.e	$$⊢E=\mathrm{Epi}\left(O\right)$$
4		oppcepi.m	$$⊢M=\mathrm{Mono}\left(C\right)$$
5	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
6	5	a1i	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
7	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
8	7	a1i	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
9	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
10	2 9	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
11		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
12	11	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
13	10 12	syl	$$⊢\phi \to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
14	6 8 2 13	monpropd	$$⊢\phi \to \mathrm{Mono}\left(C\right)=\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)$$
15	4 14	eqtrid	$$⊢\phi \to M=\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)$$
16	15	oveqd	$$⊢\phi \to YMX=Y\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)X$$
17		eqid	$$⊢\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)=\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)$$
18	11 10 17 3	oppcmon	$$⊢\phi \to Y\mathrm{Mono}\left(\mathrm{oppCat}\left(O\right)\right)X=XEY$$
19	16 18	eqtr2d	$$⊢\phi \to XEY=YMX$$