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 = { 𝑟 ∣ ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdir	⊢ DirRel
1		vr	⊢ 𝑟
2	1	cv	⊢ 𝑟
3	2	wrel	⊢ Rel 𝑟
4		cid	⊢ I
5	2	cuni	⊢ ∪ 𝑟
6	5	cuni	⊢ ∪ ∪ 𝑟
7	4 6	cres	⊢ ( I ↾ ∪ ∪ 𝑟 )
8	7 2	wss	⊢ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟
9	3 8	wa	⊢ ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 )
10	2 2	ccom	⊢ ( 𝑟 ∘ 𝑟 )
11	10 2	wss	⊢ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟
12	6 6	cxp	⊢ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 )
13	2	ccnv	⊢ ◡ 𝑟
14	13 2	ccom	⊢ ( ◡ 𝑟 ∘ 𝑟 )
15	12 14	wss	⊢ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 )
16	11 15	wa	⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) )
17	9 16	wa	⊢ ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) )
18	17 1	cab	⊢ { 𝑟 ∣ ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ) }
19	0 18	wceq	⊢ DirRel = { 𝑟 ∣ ( ( Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟 ) ⊆ 𝑟 ) ∧ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ∧ ( ∪ ∪ 𝑟 × ∪ ∪ 𝑟 ) ⊆ ( ◡ 𝑟 ∘ 𝑟 ) ) ) }