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

Definition df-inob 25964
Description: Definition of the initial objects of a category. Experimental. (Contributed by FL, 27-Jun-2014.)
Assertion
Ref Expression
df-inob  |-  InitObj  =  ( x  e.  Cat OLD  |->  { z  e.  dom  ( id_ `  x )  |  A. o  e. 
dom  ( id_ `  x
) E! m  e. 
dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  m )  =  z  /\  ( ( cod_ `  x ) `  m
)  =  o ) } )
Distinct variable group:    x, z, o, m

Detailed syntax breakdown of Definition df-inob
StepHypRef Expression
1 ciobj 25963 . 2  class  InitObj
2 vx . . 3  set  x
3 ccatOLD 25855 . . 3  class  Cat OLD
4 vm . . . . . . . . . 10  set  m
54cv 1631 . . . . . . . . 9  class  m
62cv 1631 . . . . . . . . . 10  class  x
7 cdom_ 25815 . . . . . . . . . 10  class  dom_
86, 7cfv 5271 . . . . . . . . 9  class  ( dom_ `  x )
95, 8cfv 5271 . . . . . . . 8  class  ( (
dom_ `  x ) `  m )
10 vz . . . . . . . . 9  set  z
1110cv 1631 . . . . . . . 8  class  z
129, 11wceq 1632 . . . . . . 7  wff  ( (
dom_ `  x ) `  m )  =  z
13 ccod_ 25816 . . . . . . . . . 10  class  cod_
146, 13cfv 5271 . . . . . . . . 9  class  ( cod_ `  x )
155, 14cfv 5271 . . . . . . . 8  class  ( (
cod_ `  x ) `  m )
16 vo . . . . . . . . 9  set  o
1716cv 1631 . . . . . . . 8  class  o
1815, 17wceq 1632 . . . . . . 7  wff  ( (
cod_ `  x ) `  m )  =  o
1912, 18wa 358 . . . . . 6  wff  ( ( ( dom_ `  x
) `  m )  =  z  /\  (
( cod_ `  x ) `  m )  =  o )
208cdm 4705 . . . . . 6  class  dom  ( dom_ `  x )
2119, 4, 20wreu 2558 . . . . 5  wff  E! m  e.  dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  m )  =  z  /\  ( ( cod_ `  x ) `  m
)  =  o )
22 cid_ 25817 . . . . . . 7  class  id_
236, 22cfv 5271 . . . . . 6  class  ( id_ `  x )
2423cdm 4705 . . . . 5  class  dom  ( id_ `  x )
2521, 16, 24wral 2556 . . . 4  wff  A. o  e.  dom  ( id_ `  x
) E! m  e. 
dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  m )  =  z  /\  ( ( cod_ `  x ) `  m
)  =  o )
2625, 10, 24crab 2560 . . 3  class  { z  e.  dom  ( id_ `  x )  |  A. o  e.  dom  ( id_ `  x ) E! m  e.  dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  m )  =  z  /\  ( ( cod_ `  x ) `  m
)  =  o ) }
272, 3, 26cmpt 4093 . 2  class  ( x  e.  Cat OLD  |->  { z  e.  dom  ( id_ `  x )  | 
A. o  e.  dom  ( id_ `  x ) E! m  e.  dom  ( dom_ `  x )
( ( ( dom_ `  x ) `  m
)  =  z  /\  ( ( cod_ `  x
) `  m )  =  o ) } )
281, 27wceq 1632 1  wff  InitObj  =  ( x  e.  Cat OLD  |->  { z  e.  dom  ( id_ `  x )  |  A. o  e. 
dom  ( id_ `  x
) E! m  e. 
dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  m )  =  z  /\  ( ( cod_ `  x ) `  m
)  =  o ) } )
Colors of variables: wff set class
This definition is referenced by:  isinob  25965
  Copyright terms: Public domain W3C validator