MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mon Unicode version

Definition df-mon 13633
Description: Function returning the monomorphisms of the category  c. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
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 ) ) } ) )
Distinct variable group:    b, c, f, g, h, x, y, z

Detailed syntax breakdown of Definition df-mon
StepHypRef Expression
1 cmon 13631 . 2  class Mono
2 vc . . 3  set  c
3 ccat 13566 . . 3  class  Cat
4 vb . . . 4  set  b
52cv 1622 . . . . 5  class  c
6 cbs 13148 . . . . 5  class  Base
75, 6cfv 5255 . . . 4  class  ( Base `  c )
8 vh . . . . 5  set  h
9 chom 13219 . . . . . 6  class  Hom
105, 9cfv 5255 . . . . 5  class  (  Hom  `  c )
11 vx . . . . . 6  set  x
12 vy . . . . . 6  set  y
134cv 1622 . . . . . 6  class  b
14 vg . . . . . . . . . . 11  set  g
15 vz . . . . . . . . . . . . 13  set  z
1615cv 1622 . . . . . . . . . . . 12  class  z
1711cv 1622 . . . . . . . . . . . 12  class  x
188cv 1622 . . . . . . . . . . . 12  class  h
1916, 17, 18co 5858 . . . . . . . . . . 11  class  ( z h x )
20 vf . . . . . . . . . . . . 13  set  f
2120cv 1622 . . . . . . . . . . . 12  class  f
2214cv 1622 . . . . . . . . . . . 12  class  g
2316, 17cop 3643 . . . . . . . . . . . . 13  class  <. z ,  x >.
2412cv 1622 . . . . . . . . . . . . 13  class  y
25 cco 13220 . . . . . . . . . . . . . 14  class comp
265, 25cfv 5255 . . . . . . . . . . . . 13  class  (comp `  c )
2723, 24, 26co 5858 . . . . . . . . . . . 12  class  ( <.
z ,  x >. (comp `  c ) y )
2821, 22, 27co 5858 . . . . . . . . . . 11  class  ( f ( <. z ,  x >. (comp `  c )
y ) g )
2914, 19, 28cmpt 4077 . . . . . . . . . 10  class  ( g  e.  ( z h x )  |->  ( f ( <. z ,  x >. (comp `  c )
y ) g ) )
3029ccnv 4688 . . . . . . . . 9  class  `' ( g  e.  ( z h x )  |->  ( f ( <. z ,  x >. (comp `  c
) y ) g ) )
3130wfun 5249 . . . . . . . 8  wff  Fun  `' ( g  e.  ( z h x ) 
|->  ( f ( <.
z ,  x >. (comp `  c ) y ) g ) )
3231, 15, 13wral 2543 . . . . . . 7  wff  A. z  e.  b  Fun  `' ( g  e.  ( z h x )  |->  ( f ( <. z ,  x >. (comp `  c
) y ) g ) )
3317, 24, 18co 5858 . . . . . . 7  class  ( x h y )
3432, 20, 33crab 2547 . . . . . 6  class  { f  e.  ( x h y )  |  A. z  e.  b  Fun  `' ( g  e.  ( z h x ) 
|->  ( f ( <.
z ,  x >. (comp `  c ) y ) g ) ) }
3511, 12, 13, 13, 34cmpt2 5860 . . . . 5  class  ( 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 ) ) } )
368, 10, 35csb 3081 . . . 4  class  [_ (  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 ) ) } )
374, 7, 36csb 3081 . . 3  class  [_ ( 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 ) ) } )
382, 3, 37cmpt 4077 . 2  class  ( 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 ) ) } ) )
391, 38wceq 1623 1  wff 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 ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  monfval  13635
  Copyright terms: Public domain W3C validator