Metamath Proof Explorer

Definition df-mon

Description: Function returning the monomorphisms of the category c . JFM CAT_1 def. 10. (Contributed by FL, 5-Dec-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmon 
 |-  Mono
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 cbs 
 |-  Base
4 1 cv 
 |-  c
5 4 3 cfv 
 |-  ( Base ` c )
6 vb 
 |-  b
7 chom 
 |-  Hom
8 4 7 cfv 
 |-  ( Hom ` c )
9 vh 
 |-  h
10 vx 
 |-  x
11 6 cv 
 |-  b
12 vy 
 |-  y
13 vf 
 |-  f
14 10 cv 
 |-  x
15 9 cv 
 |-  h
16 12 cv 
 |-  y
17 14 16 15 co 
 |-  ( x h y )
18 vz 
 |-  z
19 vg 
 |-  g
20 18 cv 
 |-  z
21 20 14 15 co 
 |-  ( z h x )
22 13 cv 
 |-  f
23 20 14 cop 
 |-  <. z , x >.
24 cco 
 |-  comp
25 4 24 cfv 
 |-  ( comp ` c )
26 23 16 25 co 
 |-  ( <. z , x >. ( comp ` c ) y )
27 19 cv 
 |-  g
28 22 27 26 co 
 |-  ( f ( <. z , x >. ( comp ` c ) y ) g )
29 19 21 28 cmpt 
 |-  ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) )
30 29 ccnv 
 |-  `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) )
31 30 wfun 
 |-  Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) )
32 31 18 11 wral 
 |-  A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) )
33 32 13 17 crab 
 |-  { f e. ( x h y ) | A. z e. b Fun `' ( g e. ( z h x ) |-> ( f ( <. z , x >. ( comp ` c ) y ) g ) ) }
34 10 12 11 11 33 cmpo 
 |-  ( 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 ) ) } )
35 9 8 34 csb 
 |-  [_ ( 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 ) ) } )
36 6 5 35 csb 
 |-  [_ ( 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 ) ) } )
37 1 2 36 cmpt 
 |-  ( 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 ) ) } ) )
38 0 37 wceq 
 |-  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 ) ) } ) )