MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dir Unicode version

Definition df-dir 14352
Description: Define the class of all directed sets/directions. (Contributed by Jeff Hankins, 25-Nov-2009.)
Assertion
Ref Expression
df-dir  |-  DirRel  =  {
r  |  ( ( Rel  r  /\  (  _I  |`  U. U. r
)  C_  r )  /\  ( ( r  o.  r )  C_  r  /\  ( U. U. r  X.  U. U. r ) 
C_  ( `' r  o.  r ) ) ) }

Detailed syntax breakdown of Definition df-dir
StepHypRef Expression
1 cdir 14350 . 2  class  DirRel
2 vr . . . . . . 7  set  r
32cv 1622 . . . . . 6  class  r
43wrel 4694 . . . . 5  wff  Rel  r
5 cid 4304 . . . . . . 7  class  _I
63cuni 3827 . . . . . . . 8  class  U. r
76cuni 3827 . . . . . . 7  class  U. U. r
85, 7cres 4691 . . . . . 6  class  (  _I  |`  U. U. r )
98, 3wss 3152 . . . . 5  wff  (  _I  |`  U. U. r ) 
C_  r
104, 9wa 358 . . . 4  wff  ( Rel  r  /\  (  _I  |`  U. U. r ) 
C_  r )
113, 3ccom 4693 . . . . . 6  class  ( r  o.  r )
1211, 3wss 3152 . . . . 5  wff  ( r  o.  r )  C_  r
137, 7cxp 4687 . . . . . 6  class  ( U. U. r  X.  U. U. r )
143ccnv 4688 . . . . . . 7  class  `' r
1514, 3ccom 4693 . . . . . 6  class  ( `' r  o.  r )
1613, 15wss 3152 . . . . 5  wff  ( U. U. r  X.  U. U. r )  C_  ( `' r  o.  r
)
1712, 16wa 358 . . . 4  wff  ( ( r  o.  r ) 
C_  r  /\  ( U. U. r  X.  U. U. r )  C_  ( `' r  o.  r
) )
1810, 17wa 358 . . 3  wff  ( ( Rel  r  /\  (  _I  |`  U. U. r
)  C_  r )  /\  ( ( r  o.  r )  C_  r  /\  ( U. U. r  X.  U. U. r ) 
C_  ( `' r  o.  r ) ) )
1918, 2cab 2269 . 2  class  { r  |  ( ( Rel  r  /\  (  _I  |`  U. U. r ) 
C_  r )  /\  ( ( r  o.  r )  C_  r  /\  ( U. U. r  X.  U. U. r ) 
C_  ( `' r  o.  r ) ) ) }
201, 19wceq 1623 1  wff  DirRel  =  {
r  |  ( ( Rel  r  /\  (  _I  |`  U. U. r
)  C_  r )  /\  ( ( r  o.  r )  C_  r  /\  ( U. U. r  X.  U. U. r ) 
C_  ( `' r  o.  r ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isdir  14354  dfdir2  25291
  Copyright terms: Public domain W3C validator