Metamath Proof Explorer

Theorem moni

Description: Property of a monomorphism. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses ismon.b 
|- B = ( Base ` C )
ismon.h 
|- H = ( Hom ` C )
ismon.o 
|- .x. = ( comp ` C )
ismon.s 
|- M = ( Mono ` C )
ismon.c 
|- ( ph -> C e. Cat )
ismon.x 
|- ( ph -> X e. B )
ismon.y 
|- ( ph -> Y e. B )
moni.z 
|- ( ph -> Z e. B )
moni.f 
|- ( ph -> F e. ( X M Y ) )
moni.g 
|- ( ph -> G e. ( Z H X ) )
moni.k 
|- ( ph -> K e. ( Z H X ) )
Assertion moni 
|- ( ph -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) <-> G = K ) )

Proof

Step Hyp Ref Expression
1 ismon.b 
 |-  B = ( Base ` C )
2 ismon.h 
 |-  H = ( Hom ` C )
3 ismon.o 
 |-  .x. = ( comp ` C )
4 ismon.s 
 |-  M = ( Mono ` C )
5 ismon.c 
 |-  ( ph -> C e. Cat )
6 ismon.x 
 |-  ( ph -> X e. B )
7 ismon.y 
 |-  ( ph -> Y e. B )
8 moni.z 
 |-  ( ph -> Z e. B )
9 moni.f 
 |-  ( ph -> F e. ( X M Y ) )
10 moni.g 
 |-  ( ph -> G e. ( Z H X ) )
11 moni.k 
 |-  ( ph -> K e. ( Z H X ) )
12 1 2 3 4 5 6 7 ismon2 
 |-  ( ph -> ( F e. ( X M Y ) <-> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) ) ) )
13 9 12 mpbid 
 |-  ( ph -> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) ) )
14 13 simprd 
 |-  ( ph -> A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) )
15 10 adantr 
 |-  ( ( ph /\ z = Z ) -> G e. ( Z H X ) )
16 simpr 
 |-  ( ( ph /\ z = Z ) -> z = Z )
17 16 oveq1d 
 |-  ( ( ph /\ z = Z ) -> ( z H X ) = ( Z H X ) )
18 15 17 eleqtrrd 
 |-  ( ( ph /\ z = Z ) -> G e. ( z H X ) )
19 11 adantr 
 |-  ( ( ph /\ z = Z ) -> K e. ( Z H X ) )
20 19 17 eleqtrrd 
 |-  ( ( ph /\ z = Z ) -> K e. ( z H X ) )
21 20 adantr 
 |-  ( ( ( ph /\ z = Z ) /\ g = G ) -> K e. ( z H X ) )
22 simpllr 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> z = Z )
23 22 opeq1d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> <. z , X >. = <. Z , X >. )
24 23 oveq1d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( <. z , X >. .x. Y ) = ( <. Z , X >. .x. Y ) )
25 eqidd 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> F = F )
26 simplr 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> g = G )
27 24 25 26 oveq123d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. Z , X >. .x. Y ) G ) )
28 simpr 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> h = K )
29 24 25 28 oveq123d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( F ( <. z , X >. .x. Y ) h ) = ( F ( <. Z , X >. .x. Y ) K ) )
30 27 29 eqeq12d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) <-> ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) ) )
31 26 28 eqeq12d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( g = h <-> G = K ) )
32 30 31 imbi12d 
 |-  ( ( ( ( ph /\ z = Z ) /\ g = G ) /\ h = K ) -> ( ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) <-> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) -> G = K ) ) )
33 21 32 rspcdv 
 |-  ( ( ( ph /\ z = Z ) /\ g = G ) -> ( A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) -> G = K ) ) )
34 18 33 rspcimdv 
 |-  ( ( ph /\ z = Z ) -> ( A. g e. ( z H X ) A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) -> G = K ) ) )
35 8 34 rspcimdv 
 |-  ( ph -> ( A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) -> g = h ) -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) -> G = K ) ) )
36 14 35 mpd 
 |-  ( ph -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) -> G = K ) )
37 oveq2 
 |-  ( G = K -> ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) )
38 36 37 impbid1 
 |-  ( ph -> ( ( F ( <. Z , X >. .x. Y ) G ) = ( F ( <. Z , X >. .x. Y ) K ) <-> G = K ) )