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	$$⊢\mathrm{DirRel}=\left\{r|\left(\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)\wedge \left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdir	$$class\mathrm{DirRel}$$
1		vr	$$setvarr$$
2	1	cv	$$setvarr$$
3	2	wrel	$$wff\mathrm{Rel}r$$
4		cid	$$class\mathrm{I}$$
5	2	cuni	$$class\bigcup r$$
6	5	cuni	$$class\bigcup \bigcup r$$
7	4 6	cres	$$class\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\right)$$
8	7 2	wss	$$wff{\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r$$
9	3 8	wa	$$wff\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)$$
10	2 2	ccom	$$class\left(r\circ r\right)$$
11	10 2	wss	$$wffr\circ r\subseteq r$$
12	6 6	cxp	$$class\left(\bigcup \bigcup r\times \bigcup \bigcup r\right)$$
13	2	ccnv	$$class{r}^{-1}$$
14	13 2	ccom	$$class\left(r^{-1}\circ r\right)$$
15	12 14	wss	$$wff\bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r$$
16	11 15	wa	$$wff\left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)$$
17	9 16	wa	$$wff\left(\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)\wedge \left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)\right)$$
18	17 1	cab	$$class\left\{r|\left(\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)\wedge \left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)\right)\right\}$$
19	0 18	wceq	$$wff\mathrm{DirRel}=\left\{r|\left(\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)\wedge \left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)\right)\right\}$$