Metamath Proof Explorer

Theorem ismon

Description: Definition of a monomorphism in a category. (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 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 ) ) ) ) )

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 monfval 
 |-  ( ph -> M = ( x e. B , y e. B |-> { f e. ( x H y ) | A. z e. B Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) } ) )
9 simprl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
10 simprr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
11 9 10 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x H y ) = ( X H Y ) )
12 9 oveq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( z H x ) = ( z H X ) )
13 9 opeq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> <. z , x >. = <. z , X >. )
14 13 10 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( <. z , x >. .x. y ) = ( <. z , X >. .x. Y ) )
15 14 oveqd 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( f ( <. z , x >. .x. y ) g ) = ( f ( <. z , X >. .x. Y ) g ) )
16 12 15 mpteq12dv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) = ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) )
17 16 cnveqd 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) = `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) )
18 17 funeqd 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) <-> Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) ) )
19 18 ralbidv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( A. z e. B Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) <-> A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) ) )
20 11 19 rabeqbidv 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> { 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 Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) } )
21 ovex 
 |-  ( X H Y ) e. _V
22 21 rabex 
 |-  { f e. ( X H Y ) | A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) } e. _V
23 22 a1i 
 |-  ( ph -> { f e. ( X H Y ) | A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) } e. _V )
24 8 20 6 7 23 ovmpod 
 |-  ( ph -> ( X M Y ) = { f e. ( X H Y ) | A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) } )
25 24 eleq2d 
 |-  ( ph -> ( F e. ( X M Y ) <-> F e. { f e. ( X H Y ) | A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) } ) )
26 oveq1 
 |-  ( f = F -> ( f ( <. z , X >. .x. Y ) g ) = ( F ( <. z , X >. .x. Y ) g ) )
27 26 mpteq2dv 
 |-  ( f = F -> ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) = ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) )
28 27 cnveqd 
 |-  ( f = F -> `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) = `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) )
29 28 funeqd 
 |-  ( f = F -> ( Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) <-> Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
30 29 ralbidv 
 |-  ( f = F -> ( A. z e. B Fun `' ( g e. ( z H X ) |-> ( f ( <. z , X >. .x. Y ) g ) ) <-> A. z e. B Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
31 30 elrab 
 |-  ( F e. { 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 Fun `' ( g e. ( z H X ) |-> ( F ( <. z , X >. .x. Y ) g ) ) ) )
32 25 31 bitrdi 
 |-  ( 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 ) ) ) ) )