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

Definition df-graphcatset 26025
Description: The underlying function of a morphism in the category Set. Experimental. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
df-graphcatset  |-  graph SetCat  =  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( 2nd `  a
) ) )
Distinct variable group:    x, a

Detailed syntax breakdown of Definition df-graphcatset
StepHypRef Expression
1 cgraphcase 26024 . 2  class  graph 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 . . . . 5  class  2nd
108, 9cfv 5271 . . . 4  class  ( 2nd `  a )
114, 7, 10cmpt 4093 . . 3  class  ( a  e.  ( Morphism SetCat `  x
)  |->  ( 2nd `  a
) )
122, 3, 11cmpt 4093 . 2  class  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( 2nd `  a
) ) )
131, 12wceq 1632 1  wff  graph SetCat  =  ( x  e.  Univ  |->  ( a  e.  ( Morphism SetCat `  x
)  |->  ( 2nd `  a
) ) )
Colors of variables: wff set class
This definition is referenced by:  isgraphmrph  26026
  Copyright terms: Public domain W3C validator