Metamath Proof Explorer


Theorem monpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same monomorphisms. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses monpropd.3
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
monpropd.4
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
monpropd.c
|- ( ph -> C e. Cat )
monpropd.d
|- ( ph -> D e. Cat )
Assertion monpropd
|- ( ph -> ( Mono ` C ) = ( Mono ` D ) )

Proof

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