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

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

Detailed syntax breakdown of Definition df-domcatset
StepHypRef Expression
1 cdomcase 26022 . 2  class  dom 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 c1st 6136 . . . . . 6  class  1st
109, 9ccom 4709 . . . . 5  class  ( 1st 
o.  1st )
118, 10cfv 5271 . . . 4  class  ( ( 1st  o.  1st ) `  a )
124, 7, 11cmpt 4093 . . 3  class  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 1st 
o.  1st ) `  a
) )
132, 3, 12cmpt 4093 . 2  class  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 1st 
o.  1st ) `  a
) ) )
141, 13wceq 1632 1  wff  dom SetCat  =  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( ( 1st 
o.  1st ) `  a
) ) )
Colors of variables: wff set class
This definition is referenced by:  domcatfun  26028  domcatval  26033
  Copyright terms: Public domain W3C validator