Definition df-dir 18416

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 18414	. 2 class DirRel
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1540	. . . . . 6 class 𝑟
4	3	wrel 5632	. . . . 5 wff Rel 𝑟
5		cid 5524	. . . . . . 7 class I
6	3	cuni 4860	. . . . . . . 8 class ∪ 𝑟
7	6	cuni 4860	. . . . . . 7 class ∪ ∪ 𝑟
8	5, 7	cres 5629	. . . . . 6 class ( I ↾ ∪ ∪ 𝑟)
9	8, 3	wss 3905	. . . . 5 wff ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟
10	4, 9	wa 397	. . . 4 wff (Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟)
11	3, 3	ccom 5631	. . . . . 6 class (𝑟 ∘ 𝑟)
12	11, 3	wss 3905	. . . . 5 wff (𝑟 ∘ 𝑟) ⊆ 𝑟
13	7, 7	cxp 5625	. . . . . 6 class (∪ ∪ 𝑟 × ∪ ∪ 𝑟)
14	3	ccnv 5626	. . . . . . 7 class ◡𝑟
15	14, 3	ccom 5631	. . . . . 6 class (◡𝑟 ∘ 𝑟)
16	13, 15	wss 3905	. . . . 5 wff (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)
17	12, 16	wa 397	. . . 4 wff ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟))
18	10, 17	wa 397	. . 3 wff ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))
19	18, 2	cab 2714	. 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}
20	1, 19	wceq 1541	1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}

This definition is referenced by:  isdir  18418