Step |
Hyp |
Ref |
Expression |
1 |
|
monpropd.3 |
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) ) |
2 |
|
monpropd.4 |
|- ( ph -> ( comf ` C ) = ( comf ` D ) ) |
3 |
|
monpropd.c |
|- ( ph -> C e. Cat ) |
4 |
|
monpropd.d |
|- ( ph -> D e. Cat ) |
5 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
6 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
7 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
8 |
1
|
ad2antrr |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) ) |
9 |
8
|
ad2antrr |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) ) |
10 |
|
simpr |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> c e. ( Base ` C ) ) |
11 |
|
simp-4r |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> a e. ( Base ` C ) ) |
12 |
5 6 7 9 10 11
|
homfeqval |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> ( c ( Hom ` C ) a ) = ( c ( Hom ` D ) a ) ) |
13 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
14 |
|
eqid |
|- ( comp ` D ) = ( comp ` D ) |
15 |
1
|
ad5antr |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> ( Homf ` C ) = ( Homf ` D ) ) |
16 |
2
|
ad5antr |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> ( comf ` C ) = ( comf ` D ) ) |
17 |
|
simplr |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> c e. ( Base ` C ) ) |
18 |
|
simp-5r |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> a e. ( Base ` C ) ) |
19 |
|
simp-4r |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> b e. ( Base ` C ) ) |
20 |
|
simpr |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> g e. ( c ( Hom ` C ) a ) ) |
21 |
|
simpllr |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> f e. ( a ( Hom ` C ) b ) ) |
22 |
5 6 13 14 15 16 17 18 19 20 21
|
comfeqval |
|- ( ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) /\ g e. ( c ( Hom ` C ) a ) ) -> ( f ( <. c , a >. ( comp ` C ) b ) g ) = ( f ( <. c , a >. ( comp ` D ) b ) g ) ) |
23 |
12 22
|
mpteq12dva |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) = ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) ) |
24 |
23
|
cnveqd |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) = `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) ) |
25 |
24
|
funeqd |
|- ( ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) /\ c e. ( Base ` C ) ) -> ( Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) <-> Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) ) ) |
26 |
25
|
ralbidva |
|- ( ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) /\ f e. ( a ( Hom ` C ) b ) ) -> ( A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) <-> A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) ) ) |
27 |
26
|
rabbidva |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } = { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) |
28 |
|
simplr |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> a e. ( Base ` C ) ) |
29 |
|
simpr |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> b e. ( Base ` C ) ) |
30 |
5 6 7 8 28 29
|
homfeqval |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( a ( Hom ` C ) b ) = ( a ( Hom ` D ) b ) ) |
31 |
1
|
homfeqbas |
|- ( ph -> ( Base ` C ) = ( Base ` D ) ) |
32 |
31
|
ad2antrr |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` D ) ) |
33 |
32
|
raleqdv |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) <-> A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) ) ) |
34 |
30 33
|
rabeqbidv |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } = { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) |
35 |
27 34
|
eqtrd |
|- ( ( ( ph /\ a e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } = { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) |
36 |
35
|
3impa |
|- ( ( ph /\ a e. ( Base ` C ) /\ b e. ( Base ` C ) ) -> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } = { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) |
37 |
36
|
mpoeq3dva |
|- ( ph -> ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } ) = ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) ) |
38 |
|
mpoeq12 |
|- ( ( ( Base ` C ) = ( Base ` D ) /\ ( Base ` C ) = ( Base ` D ) ) -> ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) = ( a e. ( Base ` D ) , b e. ( Base ` D ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) ) |
39 |
31 31 38
|
syl2anc |
|- ( ph -> ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) = ( a e. ( Base ` D ) , b e. ( Base ` D ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) ) |
40 |
37 39
|
eqtrd |
|- ( ph -> ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } ) = ( a e. ( Base ` D ) , b e. ( Base ` D ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) ) |
41 |
|
eqid |
|- ( Mono ` C ) = ( Mono ` C ) |
42 |
5 6 13 41 3
|
monfval |
|- ( ph -> ( Mono ` C ) = ( a e. ( Base ` C ) , b e. ( Base ` C ) |-> { f e. ( a ( Hom ` C ) b ) | A. c e. ( Base ` C ) Fun `' ( g e. ( c ( Hom ` C ) a ) |-> ( f ( <. c , a >. ( comp ` C ) b ) g ) ) } ) ) |
43 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
44 |
|
eqid |
|- ( Mono ` D ) = ( Mono ` D ) |
45 |
43 7 14 44 4
|
monfval |
|- ( ph -> ( Mono ` D ) = ( a e. ( Base ` D ) , b e. ( Base ` D ) |-> { f e. ( a ( Hom ` D ) b ) | A. c e. ( Base ` D ) Fun `' ( g e. ( c ( Hom ` D ) a ) |-> ( f ( <. c , a >. ( comp ` D ) b ) g ) ) } ) ) |
46 |
40 42 45
|
3eqtr4d |
|- ( ph -> ( Mono ` C ) = ( Mono ` D ) ) |