Theorem dirref

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

	Ref	Expression
Hypothesis	dirref.1	$$⊢X=\mathrm{dom}R$$
Assertion	dirref	$$⊢\left(R\in \mathrm{DirRel}\wedge A\in X\right)\to ARA$$

Proof

Step	Hyp	Ref	Expression
1		dirref.1	$$⊢X=\mathrm{dom}R$$
2		dirdm	$$⊢R\in \mathrm{DirRel}\to \mathrm{dom}R=\bigcup \bigcup R$$
3	1 2	syl5eq	$$⊢R\in \mathrm{DirRel}\to X=\bigcup \bigcup R$$
4	3	reseq2d	$$⊢R\in \mathrm{DirRel}\to {\mathrm{I}\upharpoonright }_X={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
5		eqid	$$⊢\bigcup \bigcup R=\bigcup \bigcup R$$
6	5	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)$$
7	6	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)$$
8	7	simplrd	$$⊢R\in \mathrm{DirRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R$$
9	4 8	eqsstrd	$$⊢R\in \mathrm{DirRel}\to {\mathrm{I}\upharpoonright }_X\subseteq R$$
10	9	ssbrd	$$⊢R\in \mathrm{DirRel}\to \left(A\left({\mathrm{I}\upharpoonright }_X\right)A\to ARA\right)$$
11		eqid	$$⊢A=A$$
12		resieq	$$⊢\left(A\in X\wedge A\in X\right)\to \left(A\left({\mathrm{I}\upharpoonright }_X\right)A\leftrightarrow A=A\right)$$
13	12	anidms	$$⊢A\in X\to \left(A\left({\mathrm{I}\upharpoonright }_X\right)A\leftrightarrow A=A\right)$$
14	11 13	mpbiri	$$⊢A\in X\to A\left({\mathrm{I}\upharpoonright }_X\right)A$$
15	10 14	impel	$$⊢\left(R\in \mathrm{DirRel}\wedge A\in X\right)\to ARA$$