Theorem oppcepi

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

	Ref	Expression
Hypotheses	oppcmon.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppcmon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	oppcepi.e	⊢ 𝐸 = ( Epi ‘ 𝑂 )
	oppcepi.m	⊢ 𝑀 = ( Mono ‘ 𝐶 )
Assertion	oppcepi	⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑌 𝑀 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcmon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		oppcepi.e	⊢ 𝐸 = ( Epi ‘ 𝑂 )
4		oppcepi.m	⊢ 𝑀 = ( Mono ‘ 𝐶 )
5	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
6	5	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
7	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
8	7	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
9	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
10	2 9	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
11		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
12	11	oppccat	⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
13	10 12	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ Cat )
14	6 8 2 13	monpropd	⊢ ( 𝜑 → ( Mono ‘ 𝐶 ) = ( Mono ‘ ( oppCat ‘ 𝑂 ) ) )
15	4 14	syl5eq	⊢ ( 𝜑 → 𝑀 = ( Mono ‘ ( oppCat ‘ 𝑂 ) ) )
16	15	oveqd	⊢ ( 𝜑 → ( 𝑌 𝑀 𝑋 ) = ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝑂 ) ) 𝑋 ) )
17		eqid	⊢ ( Mono ‘ ( oppCat ‘ 𝑂 ) ) = ( Mono ‘ ( oppCat ‘ 𝑂 ) )
18	11 10 17 3	oppcmon	⊢ ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝑂 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) )
19	16 18	eqtr2d	⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑌 𝑀 𝑋 ) )