Metamath Proof Explorer

Theorem monfval

Description: Definition of a monomorphism in a category. (Contributed by Mario Carneiro, 3-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 )
Assertion 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 ) ) } ) )

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 fvexd 
 |-  ( c = C -> ( Base ` c ) e. _V )
7 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
8 7 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
9 fvexd 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) e. _V )
10 simpl 
 |-  ( ( c = C /\ b = B ) -> c = C )
11 10 fveq2d 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
12 11 2 eqtr4di 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
13 simplr 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> b = B )
14 simpr 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> h = H )
15 14 oveqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( x h y ) = ( x H y ) )
16 14 oveqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( z h x ) = ( z H x ) )
17 simpll 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> c = C )
18 17 fveq2d 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = ( comp ` C ) )
19 18 3 eqtr4di 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = .x. )
20 19 oveqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( <. z , x >. ( comp ` c ) y ) = ( <. z , x >. .x. y ) )
21 20 oveqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( f ( <. z , x >. ( comp ` c ) y ) g ) = ( f ( <. z , x >. .x. y ) g ) )
22 16 21 mpteq12dv 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) = ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) )
23 22 cnveqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) = `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) )
24 23 funeqd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) <-> Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) ) )
25 13 24 raleqbidv 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) <-> A. z e. B Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) ) )
26 15 25 rabeqbidv 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) } = { f e. ( x H y ) | A. z e. B Fun `' ( g e. ( z H x ) |-> ( f ( <. z , x >. .x. y ) g ) ) } )
27 13 13 26 mpoeq123dv 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) } ) = ( 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 ) ) } ) )
28 9 12 27 csbied2 
 |-  ( ( c = C /\ b = B ) -> [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) } ) = ( 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 ) ) } ) )
29 6 8 28 csbied2 
 |-  ( c = C -> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) } ) = ( 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 ) ) } ) )
30 df-mon 
 |-  Mono = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ ( x e. b , y e. b |-> { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) } ) )
31 1 fvexi 
 |-  B e. _V
32 31 31 mpoex 
 |-  ( 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 ) ) } ) e. _V
33 29 30 32 fvmpt 
 |-  ( C e. Cat -> ( Mono ` C ) = ( 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 ) ) } ) )
34 5 33 syl 
 |-  ( ph -> ( Mono ` C ) = ( 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 ) ) } ) )
35 4 34 syl5eq 
 |-  ( 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 ) ) } ) )