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

Definition df-sumobj 25880
Description: " A co-product of C-objects  a and  b is a C-object  a  +  b together with a pair ( m : a --> a  +  b,  n : b --> a  +  b) of C-arrows such that for any pair of C-arrows of the form ( f : a --> c,  g : b --> c) there is exactly one arrow  [ f ,  g ] : a  +  b --> c such that  [ f ,  g ]  o.  m  =  f and  [ f ,  g ]  o.  n  =  g". Goldblatt p. 54. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-sumobj  |-  Sum Obj  =  ( c  e. 
Cat OLD  |->  ( a  e.  dom  ( id_ `  c ) ,  b  e.  dom  ( id_ `  c )  |->  { <. m ,  n >.  |  ( ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c )
)  /\  ( (
( cod_ `  c ) `  m )  =  ( ( cod_ `  c
) `  n )  /\  ( ( dom_ `  c
) `  m )  =  a  /\  (
( dom_ `  c ) `  n )  =  b )  /\  A. f  e.  dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) ) } ) )
Distinct variable group:    a, c, b, m, n, f, g, h

Detailed syntax breakdown of Definition df-sumobj
StepHypRef Expression
1 csumo 25879 . 2  class  Sum Obj
2 vc . . 3  set  c
3 ccatOLD 25752 . . 3  class  Cat OLD
4 va . . . 4  set  a
5 vb . . . 4  set  b
62cv 1622 . . . . . 6  class  c
7 cid_ 25714 . . . . . 6  class  id_
86, 7cfv 5255 . . . . 5  class  ( id_ `  c )
98cdm 4689 . . . 4  class  dom  ( id_ `  c )
10 vm . . . . . . . . 9  set  m
1110cv 1622 . . . . . . . 8  class  m
12 cdom_ 25712 . . . . . . . . . 10  class  dom_
136, 12cfv 5255 . . . . . . . . 9  class  ( dom_ `  c )
1413cdm 4689 . . . . . . . 8  class  dom  ( dom_ `  c )
1511, 14wcel 1684 . . . . . . 7  wff  m  e. 
dom  ( dom_ `  c
)
16 vn . . . . . . . . 9  set  n
1716cv 1622 . . . . . . . 8  class  n
1817, 14wcel 1684 . . . . . . 7  wff  n  e. 
dom  ( dom_ `  c
)
1915, 18wa 358 . . . . . 6  wff  ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c
) )
20 ccod_ 25713 . . . . . . . . . 10  class  cod_
216, 20cfv 5255 . . . . . . . . 9  class  ( cod_ `  c )
2211, 21cfv 5255 . . . . . . . 8  class  ( (
cod_ `  c ) `  m )
2317, 21cfv 5255 . . . . . . . 8  class  ( (
cod_ `  c ) `  n )
2422, 23wceq 1623 . . . . . . 7  wff  ( (
cod_ `  c ) `  m )  =  ( ( cod_ `  c
) `  n )
2511, 13cfv 5255 . . . . . . . 8  class  ( (
dom_ `  c ) `  m )
264cv 1622 . . . . . . . 8  class  a
2725, 26wceq 1623 . . . . . . 7  wff  ( (
dom_ `  c ) `  m )  =  a
2817, 13cfv 5255 . . . . . . . 8  class  ( (
dom_ `  c ) `  n )
295cv 1622 . . . . . . . 8  class  b
3028, 29wceq 1623 . . . . . . 7  wff  ( (
dom_ `  c ) `  n )  =  b
3124, 27, 30w3a 934 . . . . . 6  wff  ( ( ( cod_ `  c
) `  m )  =  ( ( cod_ `  c ) `  n
)  /\  ( ( dom_ `  c ) `  m )  =  a  /\  ( ( dom_ `  c ) `  n
)  =  b )
32 vf . . . . . . . . . . . . 13  set  f
3332cv 1622 . . . . . . . . . . . 12  class  f
3433, 21cfv 5255 . . . . . . . . . . 11  class  ( (
cod_ `  c ) `  f )
35 vg . . . . . . . . . . . . 13  set  g
3635cv 1622 . . . . . . . . . . . 12  class  g
3736, 21cfv 5255 . . . . . . . . . . 11  class  ( (
cod_ `  c ) `  g )
3834, 37wceq 1623 . . . . . . . . . 10  wff  ( (
cod_ `  c ) `  f )  =  ( ( cod_ `  c
) `  g )
3933, 13cfv 5255 . . . . . . . . . . 11  class  ( (
dom_ `  c ) `  f )
4039, 26wceq 1623 . . . . . . . . . 10  wff  ( (
dom_ `  c ) `  f )  =  a
4136, 13cfv 5255 . . . . . . . . . . 11  class  ( (
dom_ `  c ) `  g )
4241, 29wceq 1623 . . . . . . . . . 10  wff  ( (
dom_ `  c ) `  g )  =  b
4338, 40, 42w3a 934 . . . . . . . . 9  wff  ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )
44 vh . . . . . . . . . . . . . 14  set  h
4544cv 1622 . . . . . . . . . . . . 13  class  h
4645, 21cfv 5255 . . . . . . . . . . . 12  class  ( (
cod_ `  c ) `  h )
4746, 34wceq 1623 . . . . . . . . . . 11  wff  ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )
4845, 13cfv 5255 . . . . . . . . . . . 12  class  ( (
dom_ `  c ) `  h )
4948, 22wceq 1623 . . . . . . . . . . 11  wff  ( (
dom_ `  c ) `  h )  =  ( ( cod_ `  c
) `  m )
50 co_ 25715 . . . . . . . . . . . . . . 15  class  o_
516, 50cfv 5255 . . . . . . . . . . . . . 14  class  ( o_
`  c )
5245, 11, 51co 5858 . . . . . . . . . . . . 13  class  ( h ( o_ `  c
) m )
5352, 33wceq 1623 . . . . . . . . . . . 12  wff  ( h ( o_ `  c
) m )  =  f
5445, 17, 51co 5858 . . . . . . . . . . . . 13  class  ( h ( o_ `  c
) n )
5554, 36wceq 1623 . . . . . . . . . . . 12  wff  ( h ( o_ `  c
) n )  =  g
5653, 55wa 358 . . . . . . . . . . 11  wff  ( ( h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g )
5747, 49, 56w3a 934 . . . . . . . . . 10  wff  ( ( ( cod_ `  c
) `  h )  =  ( ( cod_ `  c ) `  f
)  /\  ( ( dom_ `  c ) `  h )  =  ( ( cod_ `  c
) `  m )  /\  ( ( h ( o_ `  c ) m )  =  f  /\  ( h ( o_ `  c ) n )  =  g ) )
5857, 44, 14wreu 2545 . . . . . . . . 9  wff  E! h  e.  dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) )
5943, 58wa 358 . . . . . . . 8  wff  ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) )
6059, 35, 14wral 2543 . . . . . . 7  wff  A. g  e.  dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) )
6160, 32, 14wral 2543 . . . . . 6  wff  A. f  e.  dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) )
6219, 31, 61w3a 934 . . . . 5  wff  ( ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c ) )  /\  ( ( ( cod_ `  c ) `  m
)  =  ( (
cod_ `  c ) `  n )  /\  (
( dom_ `  c ) `  m )  =  a  /\  ( ( dom_ `  c ) `  n
)  =  b )  /\  A. f  e. 
dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) )
6362, 10, 16copab 4076 . . . 4  class  { <. m ,  n >.  |  ( ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c )
)  /\  ( (
( cod_ `  c ) `  m )  =  ( ( cod_ `  c
) `  n )  /\  ( ( dom_ `  c
) `  m )  =  a  /\  (
( dom_ `  c ) `  n )  =  b )  /\  A. f  e.  dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) ) }
644, 5, 9, 9, 63cmpt2 5860 . . 3  class  ( a  e.  dom  ( id_ `  c ) ,  b  e.  dom  ( id_ `  c )  |->  { <. m ,  n >.  |  ( ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c )
)  /\  ( (
( cod_ `  c ) `  m )  =  ( ( cod_ `  c
) `  n )  /\  ( ( dom_ `  c
) `  m )  =  a  /\  (
( dom_ `  c ) `  n )  =  b )  /\  A. f  e.  dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) ) } )
652, 3, 64cmpt 4077 . 2  class  ( c  e.  Cat OLD  |->  ( a  e.  dom  ( id_ `  c ) ,  b  e.  dom  ( id_ `  c )  |->  {
<. m ,  n >.  |  ( ( m  e. 
dom  ( dom_ `  c
)  /\  n  e.  dom  ( dom_ `  c
) )  /\  (
( ( cod_ `  c
) `  m )  =  ( ( cod_ `  c ) `  n
)  /\  ( ( dom_ `  c ) `  m )  =  a  /\  ( ( dom_ `  c ) `  n
)  =  b )  /\  A. f  e. 
dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) ) } ) )
661, 65wceq 1623 1  wff  Sum Obj  =  ( c  e. 
Cat OLD  |->  ( a  e.  dom  ( id_ `  c ) ,  b  e.  dom  ( id_ `  c )  |->  { <. m ,  n >.  |  ( ( m  e.  dom  ( dom_ `  c )  /\  n  e.  dom  ( dom_ `  c )
)  /\  ( (
( cod_ `  c ) `  m )  =  ( ( cod_ `  c
) `  n )  /\  ( ( dom_ `  c
) `  m )  =  a  /\  (
( dom_ `  c ) `  n )  =  b )  /\  A. f  e.  dom  ( dom_ `  c
) A. g  e. 
dom  ( dom_ `  c
) ( ( ( ( cod_ `  c
) `  f )  =  ( ( cod_ `  c ) `  g
)  /\  ( ( dom_ `  c ) `  f )  =  a  /\  ( ( dom_ `  c ) `  g
)  =  b )  /\  E! h  e. 
dom  ( dom_ `  c
) ( ( (
cod_ `  c ) `  h )  =  ( ( cod_ `  c
) `  f )  /\  ( ( dom_ `  c
) `  h )  =  ( ( cod_ `  c ) `  m
)  /\  ( (
h ( o_ `  c ) m )  =  f  /\  (
h ( o_ `  c ) n )  =  g ) ) ) ) } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator