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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → 𝑀 = ( 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 ⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑌 𝑀 𝑋 ) )