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

Definition df-rocatset 25956
Description: Composition of two morphisms in the category Set. Experimental. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
df-rocatset  |-  ro SetCat  =  ( x  e.  Univ  |->  { <. <. a ,  b
>. ,  c >.  |  ( ( a  e.  ( Morphism SetCat `  x )  /\  b  e.  ( Morphism SetCat `  x )  /\  (
( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )  /\  c  =  <. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
) } )
Distinct variable group:    x, a, b, c

Detailed syntax breakdown of Definition df-rocatset
StepHypRef Expression
1 crocase 25955 . 2  class  ro SetCat
2 vx . . 3  set  x
3 cgru 8412 . . 3  class  Univ
4 va . . . . . . . 8  set  a
54cv 1622 . . . . . . 7  class  a
62cv 1622 . . . . . . . 8  class  x
7 ccmrcase 25910 . . . . . . . 8  class  Morphism SetCat
86, 7cfv 5255 . . . . . . 7  class  ( Morphism SetCat `  x )
95, 8wcel 1684 . . . . . 6  wff  a  e.  ( Morphism SetCat `  x )
10 vb . . . . . . . 8  set  b
1110cv 1622 . . . . . . 7  class  b
1211, 8wcel 1684 . . . . . 6  wff  b  e.  ( Morphism SetCat `  x )
13 c1st 6120 . . . . . . . . 9  class  1st
1413, 13ccom 4693 . . . . . . . 8  class  ( 1st 
o.  1st )
155, 14cfv 5255 . . . . . . 7  class  ( ( 1st  o.  1st ) `  a )
16 c2nd 6121 . . . . . . . . 9  class  2nd
1716, 13ccom 4693 . . . . . . . 8  class  ( 2nd 
o.  1st )
1811, 17cfv 5255 . . . . . . 7  class  ( ( 2nd  o.  1st ) `  b )
1915, 18wceq 1623 . . . . . 6  wff  ( ( 1st  o.  1st ) `  a )  =  ( ( 2nd  o.  1st ) `  b )
209, 12, 19w3a 934 . . . . 5  wff  ( a  e.  ( Morphism SetCat `  x
)  /\  b  e.  ( Morphism SetCat `  x )  /\  ( ( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )
21 vc . . . . . . 7  set  c
2221cv 1622 . . . . . 6  class  c
2311, 14cfv 5255 . . . . . . . 8  class  ( ( 1st  o.  1st ) `  b )
245, 17cfv 5255 . . . . . . . 8  class  ( ( 2nd  o.  1st ) `  a )
2523, 24cop 3643 . . . . . . 7  class  <. (
( 1st  o.  1st ) `  b ) ,  ( ( 2nd 
o.  1st ) `  a
) >.
265, 16cfv 5255 . . . . . . . 8  class  ( 2nd `  a )
2711, 16cfv 5255 . . . . . . . 8  class  ( 2nd `  b )
2826, 27ccom 4693 . . . . . . 7  class  ( ( 2nd `  a )  o.  ( 2nd `  b
) )
2925, 28cop 3643 . . . . . 6  class  <. <. (
( 1st  o.  1st ) `  b ) ,  ( ( 2nd 
o.  1st ) `  a
) >. ,  ( ( 2nd `  a )  o.  ( 2nd `  b
) ) >.
3022, 29wceq 1623 . . . . 5  wff  c  = 
<. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
3120, 30wa 358 . . . 4  wff  ( ( a  e.  ( Morphism SetCat `  x )  /\  b  e.  ( Morphism SetCat `  x )  /\  ( ( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )  /\  c  =  <. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
)
3231, 4, 10, 21coprab 5859 . . 3  class  { <. <.
a ,  b >. ,  c >.  |  ( ( a  e.  (
Morphism
SetCat `  x )  /\  b  e.  ( Morphism SetCat `  x )  /\  (
( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )  /\  c  =  <. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
) }
332, 3, 32cmpt 4077 . 2  class  ( x  e.  Univ  |->  { <. <.
a ,  b >. ,  c >.  |  ( ( a  e.  (
Morphism
SetCat `  x )  /\  b  e.  ( Morphism SetCat `  x )  /\  (
( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )  /\  c  =  <. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
) } )
341, 33wceq 1623 1  wff  ro SetCat  =  ( x  e.  Univ  |->  { <. <. a ,  b
>. ,  c >.  |  ( ( a  e.  ( Morphism SetCat `  x )  /\  b  e.  ( Morphism SetCat `  x )  /\  (
( 1st  o.  1st ) `  a )  =  ( ( 2nd 
o.  1st ) `  b
) )  /\  c  =  <. <. ( ( 1st 
o.  1st ) `  b
) ,  ( ( 2nd  o.  1st ) `  a ) >. ,  ( ( 2nd `  a
)  o.  ( 2nd `  b ) ) >.
) } )
Colors of variables: wff set class
This definition is referenced by:  isrocatset  25957
  Copyright terms: Public domain W3C validator