Definition df-dir 17230

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

Step	Hyp	Ref	Expression
1		cdir 17228	. 2 class DirRel
2		vr	. . . . . . 7 setvar r
3	2	cv 1482	. . . . . 6 class r
4	3	wrel 5119	. . . . 5 wff Rel r
5		cid 5023	. . . . . . 7 class _I
6	3	cuni 4436	. . . . . . . 8 class U. r
7	6	cuni 4436	. . . . . . 7 class U. U. r
8	5, 7	cres 5116	. . . . . 6 class ( _I |` U. U. r )
9	8, 3	wss 3574	. . . . 5 wff ( _I |` U. U. r ) C_ r
10	4, 9	wa 384	. . . 4 wff ( Rel r /\ ( _I |` U. U. r ) C_ r )
11	3, 3	ccom 5118	. . . . . 6 class ( r o. r )
12	11, 3	wss 3574	. . . . 5 wff ( r o. r ) C_ r
13	7, 7	cxp 5112	. . . . . 6 class ( U. U. r X. U. U. r )
14	3	ccnv 5113	. . . . . . 7 class `' r
15	14, 3	ccom 5118	. . . . . 6 class ( `' r o. r )
16	13, 15	wss 3574	. . . . 5 wff ( U. U. r X. U. U. r ) C_ ( `' r o. r )
17	12, 16	wa 384	. . . 4 wff ( ( r o. r ) C_ r /\ ( U. U. r X. U. U. r ) C_ ( `' r o. r ) )
18	10, 17	wa 384	. . 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 ) ) )
19	18, 2	cab 2608	. 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 ) ) ) }
20	1, 19	wceq 1483	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 ) ) ) }

This definition is referenced by:  isdir  17232