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