Theorem isdir

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

	Ref	Expression
Hypothesis	isdir.1	$$⊢A=\bigcup \bigcup R$$
Assertion	isdir	$$⊢R\in V\to \left(R\in \mathrm{DirRel}\leftrightarrow \left(\left(\mathrm{Rel}R\wedge {\mathrm{I}\upharpoonright }_A\subseteq R\right)\wedge \left(R\circ R\subseteq R\wedge A\times A\subseteq R^{-1}\circ R\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdir.1	$$⊢A=\bigcup \bigcup R$$
2		releq	$$⊢r=R\to \left(\mathrm{Rel}r\leftrightarrow \mathrm{Rel}R\right)$$
3		unieq	$$⊢r=R\to \bigcup r=\bigcup R$$
4	3	unieqd	$$⊢r=R\to \bigcup \bigcup r=\bigcup \bigcup R$$
5	4 1	eqtr4di	$$⊢r=R\to \bigcup \bigcup r=A$$
6	5	reseq2d	$$⊢r=R\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}={\mathrm{I}\upharpoonright }_A$$
7		id	$$⊢r=R\to r=R$$
8	6 7	sseq12d	$$⊢r=R\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\leftrightarrow {\mathrm{I}\upharpoonright }_A\subseteq R\right)$$
9	2 8	anbi12d	$$⊢r=R\to \left(\left(\mathrm{Rel}r\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup r}\subseteq r\right)\leftrightarrow \left(\mathrm{Rel}R\wedge {\mathrm{I}\upharpoonright }_A\subseteq R\right)\right)$$
10	7 7	coeq12d	$$⊢r=R\to r\circ r=R\circ R$$
11	10 7	sseq12d	$$⊢r=R\to \left(r\circ r\subseteq r\leftrightarrow R\circ R\subseteq R\right)$$
12	5	sqxpeqd	$$⊢r=R\to \bigcup \bigcup r\times \bigcup \bigcup r=A\times A$$
13		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
14	13 7	coeq12d	$$⊢r=R\to r^{-1}\circ r=R^{-1}\circ R$$
15	12 14	sseq12d	$$⊢r=R\to \left(\bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\leftrightarrow A\times A\subseteq R^{-1}\circ R\right)$$
16	11 15	anbi12d	$$⊢r=R\to \left(\left(r\circ r\subseteq r\wedge \bigcup \bigcup r\times \bigcup \bigcup r\subseteq r^{-1}\circ r\right)\leftrightarrow \left(R\circ R\subseteq R\wedge A\times A\subseteq R^{-1}\circ R\right)\right)$$
17	9 16	anbi12d	$$⊢r=R\to \left(\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)\leftrightarrow \left(\left(\mathrm{Rel}R\wedge {\mathrm{I}\upharpoonright }_A\subseteq R\right)\wedge \left(R\circ R\subseteq R\wedge A\times A\subseteq R^{-1}\circ R\right)\right)\right)$$
18		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\}$$
19	17 18	elab2g	$$⊢R\in V\to \left(R\in \mathrm{DirRel}\leftrightarrow \left(\left(\mathrm{Rel}R\wedge {\mathrm{I}\upharpoonright }_A\subseteq R\right)\wedge \left(R\circ R\subseteq R\wedge A\times A\subseteq R^{-1}\circ R\right)\right)\right)$$