Definition df-dir 18641

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 18639	. 2 class DirRel
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1539	. . . . . 6 class 𝑟
4	3	wrel 5690	. . . . 5 wff Rel 𝑟
5		cid 5577	. . . . . . 7 class I
6	3	cuni 4907	. . . . . . . 8 class ∪ 𝑟
7	6	cuni 4907	. . . . . . 7 class ∪ ∪ 𝑟
8	5, 7	cres 5687	. . . . . 6 class ( I ↾ ∪ ∪ 𝑟)
9	8, 3	wss 3951	. . . . 5 wff ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟
10	4, 9	wa 395	. . . 4 wff (Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟)
11	3, 3	ccom 5689	. . . . . 6 class (𝑟 ∘ 𝑟)
12	11, 3	wss 3951	. . . . 5 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
13	7, 7	cxp 5683	. . . . . 6 class (∪ ∪ 𝑟 × ∪ ∪ 𝑟)
14	3	ccnv 5684	. . . . . . 7 class ◡𝑟
15	14, 3	ccom 5689	. . . . . 6 class (◡𝑟 ∘ 𝑟)
16	13, 15	wss 3951	. . . . 5 wff (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)
17	12, 16	wa 395	. . . 4 wff ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟))
18	10, 17	wa 395	. . 3 wff ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))
19	18, 2	cab 2714	. 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}
20	1, 19	wceq 1540	1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}

This definition is referenced by:  isdir  18643