This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝐸 = tpos 𝑀 )
16 15 oveqd ⊢ ( 𝜑 → ( 𝑌 𝐸 𝑋 ) = ( 𝑌 tpos 𝑀 𝑋 ) )
17 ovtpos ⊢ ( 𝑌 tpos 𝑀 𝑋 ) = ( 𝑋 𝑀 𝑌 )
18 16 17 eqtr2di ⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑌 𝐸 𝑋 ) )