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 
|- 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 ) )