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

Definition df-morcatset 26014
Description: The morphisms of the category Set. ( a is redundant and could be retrieved from  c.) Experimental. (Contributed by FL, 15-Sep-2013.)
Assertion
Ref Expression
df-morcatset  |-  Morphism SetCat  =  ( x  e.  Univ  |->  { <. <.
a ,  b >. ,  c >.  |  ( a  e.  x  /\  b  e.  x  /\  c  e.  ( b  ^m  a ) ) } )
Distinct variable group:    x, a, b, c

Detailed syntax breakdown of Definition df-morcatset
StepHypRef Expression
1 ccmrcase 26013 . 2  class  Morphism SetCat
2 vx . . 3  set  x
3 cgru 8428 . . 3  class  Univ
4 va . . . . . 6  set  a
54, 2wel 1697 . . . . 5  wff  a  e.  x
6 vb . . . . . 6  set  b
76, 2wel 1697 . . . . 5  wff  b  e.  x
8 vc . . . . . . 7  set  c
98cv 1631 . . . . . 6  class  c
106cv 1631 . . . . . . 7  class  b
114cv 1631 . . . . . . 7  class  a
12 cmap 6788 . . . . . . 7  class  ^m
1310, 11, 12co 5874 . . . . . 6  class  ( b  ^m  a )
149, 13wcel 1696 . . . . 5  wff  c  e.  ( b  ^m  a
)
155, 7, 14w3a 934 . . . 4  wff  ( a  e.  x  /\  b  e.  x  /\  c  e.  ( b  ^m  a
) )
1615, 4, 6, 8coprab 5875 . . 3  class  { <. <.
a ,  b >. ,  c >.  |  ( a  e.  x  /\  b  e.  x  /\  c  e.  ( b  ^m  a ) ) }
172, 3, 16cmpt 4093 . 2  class  ( x  e.  Univ  |->  { <. <.
a ,  b >. ,  c >.  |  ( a  e.  x  /\  b  e.  x  /\  c  e.  ( b  ^m  a ) ) } )
181, 17wceq 1632 1  wff  Morphism SetCat  =  ( x  e.  Univ  |->  { <. <.
a ,  b >. ,  c >.  |  ( a  e.  x  /\  b  e.  x  /\  c  e.  ( b  ^m  a ) ) } )
Colors of variables: wff set class
This definition is referenced by:  prismorcset  26017  morcatset1  26018  domcatfun  26028  codcatfun  26037
  Copyright terms: Public domain W3C validator