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

Proof

Step Hyp Ref Expression
1 oppcmon.o
 |-  O = ( oppCat ` C )
2 oppcmon.c
 |-  ( ph -> C e. Cat )
3 oppcmon.m
 |-  M = ( Mono ` O )
4 oppcmon.e
 |-  E = ( Epi ` C )
5 fveq2
 |-  ( c = C -> ( oppCat ` c ) = ( oppCat ` C ) )
6 5 1 eqtr4di
 |-  ( c = C -> ( oppCat ` c ) = O )
7 6 fveq2d
 |-  ( c = C -> ( Mono ` ( oppCat ` c ) ) = ( Mono ` O ) )
8 7 3 eqtr4di
 |-  ( c = C -> ( Mono ` ( oppCat ` c ) ) = M )
9 8 tposeqd
 |-  ( c = C -> tpos ( Mono ` ( oppCat ` c ) ) = tpos M )
10 df-epi
 |-  Epi = ( c e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) )
11 3 fvexi
 |-  M e. _V
12 11 tposex
 |-  tpos M e. _V
13 9 10 12 fvmpt
 |-  ( C e. Cat -> ( Epi ` C ) = tpos M )
14 2 13 syl
 |-  ( ph -> ( Epi ` C ) = tpos M )
15 4 14 eqtrid
 |-  ( ph -> E = tpos M )
16 15 oveqd
 |-  ( ph -> ( Y E X ) = ( Y tpos M X ) )
17 ovtpos
 |-  ( Y tpos M X ) = ( X M Y )
18 16 17 eqtr2di
 |-  ( ph -> ( X M Y ) = ( Y E X ) )