Metamath Proof Explorer

Theorem ismon2

Description: Write out the monomorphism property directly. (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 )
Assertion 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 ) ) ) )

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 1 2 3 4 5 6 7 ismon 
 |-  ( ph -> ( F e. ( X M Y ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) ) )
9 5 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> C e. Cat )
10 simprl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> z e. B )
11 6 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> X e. B )
12 7 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> Y e. B )
13 simprr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> g e. ( z H X ) )
14 simplr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> F e. ( X H Y ) )
15 1 2 3 9 10 11 12 13 14 catcocl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( z H X ) ) ) -> ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) )
16 15 anassrs 
 |-  ( ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) /\ g e. ( z H X ) ) -> ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) )
17 16 ralrimiva 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) -> A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) )
18 eqid 
 |-  ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) = ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) )
19 18 fmpt 
 |-  ( A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) <-> ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) --> ( z H Y ) )
20 df-f1 
 |-  ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) -1-1-> ( z H Y ) <-> ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) --> ( z H Y ) /\ Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
21 20 baib 
 |-  ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) --> ( z H Y ) -> ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) -1-1-> ( z H Y ) <-> Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
22 19 21 sylbi 
 |-  ( A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) -> ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) -1-1-> ( z H Y ) <-> Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
23 oveq2 
 |-  ( g = h -> ( F ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) h ) )
24 18 23 f1mpt 
 |-  ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) -1-1-> ( z H Y ) <-> ( A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) /\ 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 ) ) )
25 24 baib 
 |-  ( A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) -> ( ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) : ( z H X ) -1-1-> ( z H Y ) <-> 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 ) ) )
26 22 25 bitr3d 
 |-  ( A. g e. ( z H X ) ( F ( <. z , X >. .x. Y ) g ) e. ( z H Y ) -> ( Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) <-> 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 ) ) )
27 17 26 syl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) -> ( Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) <-> 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 ) ) )
28 27 ralbidva 
 |-  ( ( ph /\ F e. ( X H Y ) ) -> ( A. z e. B Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) <-> 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 ) ) )
29 28 pm5.32da 
 |-  ( ph -> ( ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) <-> ( 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 ) ) ) )
30 8 29 bitrd 
 |-  ( 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 ) ) ) )