Theorem reldir

Description: A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Assertion	reldir	$$⊢R\in \mathrm{DirRel}\to \mathrm{Rel}R$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup \bigcup R=\bigcup \bigcup R$$
2	1	isdir	$$⊢R\in \mathrm{DirRel}\to \left(R\in \mathrm{DirRel}\leftrightarrow \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)$$
3	2	ibi	$$⊢R\in \mathrm{DirRel}\to \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)$$
4	3	simplld	$$⊢R\in \mathrm{DirRel}\to \mathrm{Rel}R$$