Theorem oppcmon

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

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

Proof

Step	Hyp	Ref	Expression
1		oppcmon.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcmon.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		oppcmon.m	⊢ 𝑀 = ( Mono ‘ 𝑂 )
4		oppcmon.e	⊢ 𝐸 = ( Epi ‘ 𝐶 )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝐶 ) )
6	5 1	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( oppCat ‘ 𝑐 ) = 𝑂 )
7	6	fveq2d	⊢ ( 𝑐 = 𝐶 → ( Mono ‘ ( oppCat ‘ 𝑐 ) ) = ( Mono ‘ 𝑂 ) )
8	7 3	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Mono ‘ ( oppCat ‘ 𝑐 ) ) = 𝑀 )
9	8	tposeqd	⊢ ( 𝑐 = 𝐶 → tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) = tpos 𝑀 )
10		df-epi	⊢ Epi = ( 𝑐 ∈ Cat ↦ tpos ( Mono ‘ ( oppCat ‘ 𝑐 ) ) )
11	3	fvexi	⊢ 𝑀 ∈ V
12	11	tposex	⊢ tpos 𝑀 ∈ V
13	9 10 12	fvmpt	⊢ ( 𝐶 ∈ Cat → ( Epi ‘ 𝐶 ) = tpos 𝑀 )
14	2 13	syl	⊢ ( 𝜑 → ( Epi ‘ 𝐶 ) = tpos 𝑀 )
15	4 14	syl5eq	⊢ ( 𝜑 → 𝐸 = tpos 𝑀 )
16	15	oveqd	⊢ ( 𝜑 → ( 𝑌 𝐸 𝑋 ) = ( 𝑌 tpos 𝑀 𝑋 ) )
17		ovtpos	⊢ ( 𝑌 tpos 𝑀 𝑋 ) = ( 𝑋 𝑀 𝑌 )
18	16 17	eqtr2di	⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑌 𝐸 𝑋 ) )