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 O = oppCat C
oppcmon.c φ C Cat
oppcepi.e E = Epi O
oppcepi.m M = Mono C
Assertion oppcepi φ X E Y = Y M X

Proof

Step Hyp Ref Expression
1 oppcmon.o O = oppCat C
2 oppcmon.c φ C Cat
3 oppcepi.e E = Epi O
4 oppcepi.m M = Mono C
5 1 2oppchomf Hom 𝑓 C = Hom 𝑓 oppCat O
6 5 a1i φ Hom 𝑓 C = Hom 𝑓 oppCat O
7 1 2oppccomf comp 𝑓 C = comp 𝑓 oppCat O
8 7 a1i φ comp 𝑓 C = comp 𝑓 oppCat O
9 1 oppccat C Cat O Cat
10 2 9 syl φ O Cat
11 eqid oppCat O = oppCat O
12 11 oppccat O Cat oppCat O Cat
13 10 12 syl φ oppCat O Cat
14 6 8 2 13 monpropd φ Mono C = Mono oppCat O
15 4 14 eqtrid φ M = Mono oppCat O
16 15 oveqd φ Y M X = Y Mono oppCat O X
17 eqid Mono oppCat O = Mono oppCat O
18 11 10 17 3 oppcmon φ Y Mono oppCat O X = X E Y
19 16 18 eqtr2d φ X E Y = Y M X