Step |
Hyp |
Ref |
Expression |
1 |
|
isepi.b |
|- B = ( Base ` C ) |
2 |
|
isepi.h |
|- H = ( Hom ` C ) |
3 |
|
isepi.o |
|- .x. = ( comp ` C ) |
4 |
|
isepi.e |
|- E = ( Epi ` C ) |
5 |
|
isepi.c |
|- ( ph -> C e. Cat ) |
6 |
|
isepi.x |
|- ( ph -> X e. B ) |
7 |
|
isepi.y |
|- ( ph -> Y e. B ) |
8 |
|
eqid |
|- ( oppCat ` C ) = ( oppCat ` C ) |
9 |
8 1
|
oppcbas |
|- B = ( Base ` ( oppCat ` C ) ) |
10 |
|
eqid |
|- ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) ) |
11 |
|
eqid |
|- ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) ) |
12 |
|
eqid |
|- ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) ) |
13 |
8
|
oppccat |
|- ( C e. Cat -> ( oppCat ` C ) e. Cat ) |
14 |
5 13
|
syl |
|- ( ph -> ( oppCat ` C ) e. Cat ) |
15 |
9 10 11 12 14 7 6
|
ismon |
|- ( ph -> ( F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) <-> ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) /\ A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) ) ) ) |
16 |
8 5 12 4
|
oppcmon |
|- ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) ) |
17 |
16
|
eleq2d |
|- ( ph -> ( F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) <-> F e. ( X E Y ) ) ) |
18 |
2 8
|
oppchom |
|- ( Y ( Hom ` ( oppCat ` C ) ) X ) = ( X H Y ) |
19 |
18
|
a1i |
|- ( ph -> ( Y ( Hom ` ( oppCat ` C ) ) X ) = ( X H Y ) ) |
20 |
19
|
eleq2d |
|- ( ph -> ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) <-> F e. ( X H Y ) ) ) |
21 |
2 8
|
oppchom |
|- ( z ( Hom ` ( oppCat ` C ) ) Y ) = ( Y H z ) |
22 |
21
|
a1i |
|- ( ( ph /\ z e. B ) -> ( z ( Hom ` ( oppCat ` C ) ) Y ) = ( Y H z ) ) |
23 |
|
simpr |
|- ( ( ph /\ z e. B ) -> z e. B ) |
24 |
7
|
adantr |
|- ( ( ph /\ z e. B ) -> Y e. B ) |
25 |
6
|
adantr |
|- ( ( ph /\ z e. B ) -> X e. B ) |
26 |
1 3 8 23 24 25
|
oppcco |
|- ( ( ph /\ z e. B ) -> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) = ( g ( <. X , Y >. .x. z ) F ) ) |
27 |
22 26
|
mpteq12dv |
|- ( ( ph /\ z e. B ) -> ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) = ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) |
28 |
27
|
cnveqd |
|- ( ( ph /\ z e. B ) -> `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) = `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) |
29 |
28
|
funeqd |
|- ( ( ph /\ z e. B ) -> ( Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) <-> Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) |
30 |
29
|
ralbidva |
|- ( ph -> ( A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) <-> A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) |
31 |
20 30
|
anbi12d |
|- ( ph -> ( ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) /\ A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) ) |
32 |
15 17 31
|
3bitr3d |
|- ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) ) |