Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-monOLD Unicode version

Definition df-monOLD 25806
Description: Function returning the monomorphisms of the category  x. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.)
Assertion
Ref Expression
df-monOLD  |- MonoOLD  =  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x
) ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) ) } )
Distinct variable group:    x, f, g, h

Detailed syntax breakdown of Definition df-monOLD
StepHypRef Expression
1 cmonOLD 25804 . 2  class MonoOLD
2 vx . . 3  set  x
3 ccatOLD 25752 . . 3  class  Cat OLD
4 vg . . . . . . . . . . 11  set  g
54cv 1622 . . . . . . . . . 10  class  g
62cv 1622 . . . . . . . . . . 11  class  x
7 cdom_ 25712 . . . . . . . . . . 11  class  dom_
86, 7cfv 5255 . . . . . . . . . 10  class  ( dom_ `  x )
95, 8cfv 5255 . . . . . . . . 9  class  ( (
dom_ `  x ) `  g )
10 vh . . . . . . . . . . 11  set  h
1110cv 1622 . . . . . . . . . 10  class  h
1211, 8cfv 5255 . . . . . . . . 9  class  ( (
dom_ `  x ) `  h )
139, 12wceq 1623 . . . . . . . 8  wff  ( (
dom_ `  x ) `  g )  =  ( ( dom_ `  x
) `  h )
14 ccod_ 25713 . . . . . . . . . . 11  class  cod_
156, 14cfv 5255 . . . . . . . . . 10  class  ( cod_ `  x )
165, 15cfv 5255 . . . . . . . . 9  class  ( (
cod_ `  x ) `  g )
17 vf . . . . . . . . . . 11  set  f
1817cv 1622 . . . . . . . . . 10  class  f
1918, 8cfv 5255 . . . . . . . . 9  class  ( (
dom_ `  x ) `  f )
2016, 19wceq 1623 . . . . . . . 8  wff  ( (
cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )
2111, 15cfv 5255 . . . . . . . . 9  class  ( (
cod_ `  x ) `  h )
2221, 19wceq 1623 . . . . . . . 8  wff  ( (
cod_ `  x ) `  h )  =  ( ( dom_ `  x
) `  f )
2313, 20, 22w3a 934 . . . . . . 7  wff  ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )
24 co_ 25715 . . . . . . . . . . 11  class  o_
256, 24cfv 5255 . . . . . . . . . 10  class  ( o_
`  x )
2618, 5, 25co 5858 . . . . . . . . 9  class  ( f ( o_ `  x
) g )
2718, 11, 25co 5858 . . . . . . . . 9  class  ( f ( o_ `  x
) h )
2826, 27wceq 1623 . . . . . . . 8  wff  ( f ( o_ `  x
) g )  =  ( f ( o_
`  x ) h )
294, 10weq 1624 . . . . . . . 8  wff  g  =  h
3028, 29wi 4 . . . . . . 7  wff  ( ( f ( o_ `  x ) g )  =  ( f ( o_ `  x ) h )  ->  g  =  h )
3123, 30wi 4 . . . . . 6  wff  ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) )
328cdm 4689 . . . . . 6  class  dom  ( dom_ `  x )
3331, 10, 32wral 2543 . . . . 5  wff  A. h  e.  dom  ( dom_ `  x
) ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) )
3433, 4, 32wral 2543 . . . 4  wff  A. g  e.  dom  ( dom_ `  x
) A. h  e. 
dom  ( dom_ `  x
) ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) )
3534, 17, 32crab 2547 . . 3  class  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x
) ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) ) }
362, 3, 35cmpt 4077 . 2  class  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  | 
A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x )
( ( ( (
dom_ `  x ) `  g )  =  ( ( dom_ `  x
) `  h )  /\  ( ( cod_ `  x
) `  g )  =  ( ( dom_ `  x ) `  f
)  /\  ( ( cod_ `  x ) `  h )  =  ( ( dom_ `  x
) `  f )
)  ->  ( (
f ( o_ `  x ) g )  =  ( f ( o_ `  x ) h )  ->  g  =  h ) ) } )
371, 36wceq 1623 1  wff MonoOLD  =  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x
) ( ( ( ( dom_ `  x
) `  g )  =  ( ( dom_ `  x ) `  h
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  h )  =  ( ( dom_ `  x ) `  f
) )  ->  (
( f ( o_
`  x ) g )  =  ( f ( o_ `  x
) h )  -> 
g  =  h ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ismona  25809
  Copyright terms: Public domain W3C validator