Definition df-dir 18687

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.)

Assertion

Ref	Expression
df-dir	⊢ DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}

Detailed syntax breakdown of Definition df-dir

Step	Hyp	Ref	Expression
1		cdir 18685	. 2 class DirRel
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1569	. . . . . 6 class 𝑟
4	3	wrel 5660	. . . . 5 wff Rel 𝑟
5		cid 5549	. . . . . . 7 class I
6	3	cuni 4867	. . . . . . . 8 class ∪ 𝑟
7	6	cuni 4867	. . . . . . 7 class ∪ ∪ 𝑟
8	5, 7	cres 5657	. . . . . 6 class ( I ↾ ∪ ∪ 𝑟)
9	8, 3	wss 3899	. . . . 5 wff ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟
10	4, 9	wa 401	. . . 4 wff (Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟)
11	3, 3	ccom 5659	. . . . . 6 class (𝑟 ∘ 𝑟)
12	11, 3	wss 3899	. . . . 5 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
13	7, 7	cxp 5653	. . . . . 6 class (∪ ∪ 𝑟 × ∪ ∪ 𝑟)
14	3	ccnv 5654	. . . . . . 7 class ◡𝑟
15	14, 3	ccom 5659	. . . . . 6 class (◡𝑟 ∘ 𝑟)
16	13, 15	wss 3899	. . . . 5 wff (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)
17	12, 16	wa 401	. . . 4 wff ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟))
18	10, 17	wa 401	. . 3 wff ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))
19	18, 2	cab 2738	. 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}
20	1, 19	wceq 1570	1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}

This definition is used by:  isdir  18689