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

Definition df-epiOLD 25910
Description: Function returning the epimorphisms of the category  x. JFM CAT1 def. 11. (Contributed by FL, 8-Aug-2008.)
Assertion
Ref Expression
df-epiOLD  |- Epic  =  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x )
( ( ( (
cod_ `  x ) `  g )  =  ( ( cod_ `  x
) `  h )  /\  ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( dom_ `  x ) `  h )  =  ( ( cod_ `  x
) `  f )
)  ->  ( (
g ( o_ `  x ) f )  =  ( h ( o_ `  x ) f )  ->  g  =  h ) ) } )
Distinct variable group:    x, f, g, h

Detailed syntax breakdown of Definition df-epiOLD
StepHypRef Expression
1 cepiOLD 25906 . 2  class Epic
2 vx . . 3  set  x
3 ccatOLD 25855 . . 3  class  Cat OLD
4 vg . . . . . . . . . . 11  set  g
54cv 1631 . . . . . . . . . 10  class  g
62cv 1631 . . . . . . . . . . 11  class  x
7 ccod_ 25816 . . . . . . . . . . 11  class  cod_
86, 7cfv 5271 . . . . . . . . . 10  class  ( cod_ `  x )
95, 8cfv 5271 . . . . . . . . 9  class  ( (
cod_ `  x ) `  g )
10 vh . . . . . . . . . . 11  set  h
1110cv 1631 . . . . . . . . . 10  class  h
1211, 8cfv 5271 . . . . . . . . 9  class  ( (
cod_ `  x ) `  h )
139, 12wceq 1632 . . . . . . . 8  wff  ( (
cod_ `  x ) `  g )  =  ( ( cod_ `  x
) `  h )
14 cdom_ 25815 . . . . . . . . . . 11  class  dom_
156, 14cfv 5271 . . . . . . . . . 10  class  ( dom_ `  x )
165, 15cfv 5271 . . . . . . . . 9  class  ( (
dom_ `  x ) `  g )
17 vf . . . . . . . . . . 11  set  f
1817cv 1631 . . . . . . . . . 10  class  f
1918, 8cfv 5271 . . . . . . . . 9  class  ( (
cod_ `  x ) `  f )
2016, 19wceq 1632 . . . . . . . 8  wff  ( (
dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )
2111, 15cfv 5271 . . . . . . . . 9  class  ( (
dom_ `  x ) `  h )
2221, 19wceq 1632 . . . . . . . 8  wff  ( (
dom_ `  x ) `  h )  =  ( ( cod_ `  x
) `  f )
2313, 20, 22w3a 934 . . . . . . 7  wff  ( ( ( cod_ `  x
) `  g )  =  ( ( cod_ `  x ) `  h
)  /\  ( ( dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( dom_ `  x
) `  h )  =  ( ( cod_ `  x ) `  f
) )
24 co_ 25818 . . . . . . . . . . 11  class  o_
256, 24cfv 5271 . . . . . . . . . 10  class  ( o_
`  x )
265, 18, 25co 5874 . . . . . . . . 9  class  ( g ( o_ `  x
) f )
2711, 18, 25co 5874 . . . . . . . . 9  class  ( h ( o_ `  x
) f )
2826, 27wceq 1632 . . . . . . . 8  wff  ( g ( o_ `  x
) f )  =  ( h ( o_
`  x ) f )
294, 10weq 1633 . . . . . . . 8  wff  g  =  h
3028, 29wi 4 . . . . . . 7  wff  ( ( g ( o_ `  x ) f )  =  ( h ( o_ `  x ) f )  ->  g  =  h )
3123, 30wi 4 . . . . . 6  wff  ( ( ( ( cod_ `  x
) `  g )  =  ( ( cod_ `  x ) `  h
)  /\  ( ( dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( dom_ `  x
) `  h )  =  ( ( cod_ `  x ) `  f
) )  ->  (
( g ( o_
`  x ) f )  =  ( h ( o_ `  x
) f )  -> 
g  =  h ) )
3215cdm 4705 . . . . . 6  class  dom  ( dom_ `  x )
3331, 10, 32wral 2556 . . . . 5  wff  A. h  e.  dom  ( dom_ `  x
) ( ( ( ( cod_ `  x
) `  g )  =  ( ( cod_ `  x ) `  h
)  /\  ( ( dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( dom_ `  x
) `  h )  =  ( ( cod_ `  x ) `  f
) )  ->  (
( g ( o_
`  x ) f )  =  ( h ( o_ `  x
) f )  -> 
g  =  h ) )
3433, 4, 32wral 2556 . . . 4  wff  A. g  e.  dom  ( dom_ `  x
) A. h  e. 
dom  ( dom_ `  x
) ( ( ( ( cod_ `  x
) `  g )  =  ( ( cod_ `  x ) `  h
)  /\  ( ( dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( dom_ `  x
) `  h )  =  ( ( cod_ `  x ) `  f
) )  ->  (
( g ( o_
`  x ) f )  =  ( h ( o_ `  x
) f )  -> 
g  =  h ) )
3534, 17, 32crab 2560 . . 3  class  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x
) ( ( ( ( cod_ `  x
) `  g )  =  ( ( cod_ `  x ) `  h
)  /\  ( ( dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( dom_ `  x
) `  h )  =  ( ( cod_ `  x ) `  f
) )  ->  (
( g ( o_
`  x ) f )  =  ( h ( o_ `  x
) f )  -> 
g  =  h ) ) }
362, 3, 35cmpt 4093 . 2  class  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  | 
A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x )
( ( ( (
cod_ `  x ) `  g )  =  ( ( cod_ `  x
) `  h )  /\  ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( dom_ `  x ) `  h )  =  ( ( cod_ `  x
) `  f )
)  ->  ( (
g ( o_ `  x ) f )  =  ( h ( o_ `  x ) f )  ->  g  =  h ) ) } )
371, 36wceq 1632 1  wff Epic  =  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  A. g  e.  dom  ( dom_ `  x ) A. h  e.  dom  ( dom_ `  x )
( ( ( (
cod_ `  x ) `  g )  =  ( ( cod_ `  x
) `  h )  /\  ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( dom_ `  x ) `  h )  =  ( ( cod_ `  x
) `  f )
)  ->  ( (
g ( o_ `  x ) f )  =  ( h ( o_ `  x ) f )  ->  g  =  h ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isepia  25922
  Copyright terms: Public domain W3C validator