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

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcmon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		oppcmon.m	$$⊢M=\mathrm{Mono}\left(O\right)$$
4		oppcmon.e	$$⊢E=\mathrm{Epi}\left(C\right)$$
5		fveq2	$$⊢c=C\to \mathrm{oppCat}\left(c\right)=\mathrm{oppCat}\left(C\right)$$
6	5 1	eqtr4di	$$⊢c=C\to \mathrm{oppCat}\left(c\right)=O$$
7	6	fveq2d	$$⊢c=C\to \mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)=\mathrm{Mono}\left(O\right)$$
8	7 3	eqtr4di	$$⊢c=C\to \mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)=M$$
9	8	tposeqd	$$⊢c=C\to tpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)=tposM$$
10		df-epi	$$⊢\mathrm{Epi}=\left(c\in \mathrm{Cat}⟼tpos\mathrm{Mono}\left(\mathrm{oppCat}\left(c\right)\right)\right)$$
11	3	fvexi	$$⊢M\in \mathrm{V}$$
12	11	tposex	$$⊢tposM\in \mathrm{V}$$
13	9 10 12	fvmpt	$$⊢C\in \mathrm{Cat}\to \mathrm{Epi}\left(C\right)=tposM$$
14	2 13	syl	$$⊢\phi \to \mathrm{Epi}\left(C\right)=tposM$$
15	4 14	eqtrid	$$⊢\phi \to E=tposM$$
16	15	oveqd	$$⊢\phi \to YEX=YtposMX$$
17		ovtpos	$$⊢YtposMX=XMY$$
18	16 17	eqtr2di	$$⊢\phi \to XMY=YEX$$