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