Metamath Proof Explorer

Definition df-dir

Description: Define the class of directed sets (the order relation itself is sometimes called a direction, and a directed set is a set equipped with a direction). (Contributed by Jeff Hankins, 25-Nov-2009)

Ref Expression
Assertion 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

Step Hyp Ref Expression
0 cdir 
 |-  DirRel
1 vr 
 |-  r
2 1 cv 
 |-  r
3 2 wrel 
 |-  Rel r
4 cid 
 |-  _I
5 2 cuni 
 |-  U. r
6 5 cuni 
 |-  U. U. r
7 4 6 cres 
 |-  ( _I |` U. U. r )
8 7 2 wss 
 |-  ( _I |` U. U. r ) C_ r
9 3 8 wa 
 |-  ( Rel r /\ ( _I |` U. U. r ) C_ r )
10 2 2 ccom 
 |-  ( r o. r )
11 10 2 wss 
 |-  ( r o. r ) C_ r
12 6 6 cxp 
 |-  ( U. U. r X. U. U. r )
13 2 ccnv 
 |-  `' r
14 13 2 ccom 
 |-  ( `' r o. r )
15 12 14 wss 
 |-  ( U. U. r X. U. U. r ) C_ ( `' r o. r )
16 11 15 wa 
 |-  ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) )
17 9 16 wa 
 |-  ( ( Rel r /\ ( _I |` U. U. r ) C_ r ) /\ ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) ) )
18 17 1 cab 
 |-  { 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 ) ) ) }
19 0 18 wceq 
 |-  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 ) ) ) }