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

Definition df-codcatset 26036
Description: The codomain of a morphism in the category Set. Experimental. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
df-codcatset  |-  cod SetCat  =  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 2nd 
o.  1st ) `  a
) ) )
Distinct variable group:    x, a

Detailed syntax breakdown of Definition df-codcatset
StepHypRef Expression
1 ccodcase 26035 . 2  class  cod SetCat
2 vx . . 3  set  x
3 cgru 8428 . . 3  class  Univ
4 va . . . 4  set  a
52cv 1631 . . . . 5  class  x
6 ccmrcase 26013 . . . . 5  class  Morphism SetCat
75, 6cfv 5271 . . . 4  class  ( Morphism SetCat `  x )
84cv 1631 . . . . 5  class  a
9 c2nd 6137 . . . . . 6  class  2nd
10 c1st 6136 . . . . . 6  class  1st
119, 10ccom 4709 . . . . 5  class  ( 2nd 
o.  1st )
128, 11cfv 5271 . . . 4  class  ( ( 2nd  o.  1st ) `  a )
134, 7, 12cmpt 4093 . . 3  class  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 2nd 
o.  1st ) `  a
) )
142, 3, 13cmpt 4093 . 2  class  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 2nd 
o.  1st ) `  a
) ) )
151, 14wceq 1632 1  wff  cod SetCat  =  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 2nd 
o.  1st ) `  a
) ) )
Colors of variables: wff set class
This definition is referenced by:  codcatfun  26037  codcatval  26039
  Copyright terms: Public domain W3C validator