Theorem dirdm

Description: A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Assertion	dirdm	$$⊢R\in \mathrm{DirRel}\to \mathrm{dom}R=\bigcup \bigcup R$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢\mathrm{dom}R\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
2		dmrnssfld	$$⊢\mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R$$
3	1 2	sstri	$$⊢\mathrm{dom}R\subseteq \bigcup \bigcup R$$
4	3	a1i	$$⊢R\in \mathrm{DirRel}\to \mathrm{dom}R\subseteq \bigcup \bigcup R$$
5		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)=\bigcup \bigcup R$$
6		eqid	$$⊢\bigcup \bigcup R=\bigcup \bigcup R$$
7	6	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)$$
8	7	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)$$
9	8	simplrd	$$⊢R\in \mathrm{DirRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R$$
10		dmss	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R\to \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\subseteq \mathrm{dom}R$$
11	9 10	syl	$$⊢R\in \mathrm{DirRel}\to \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\subseteq \mathrm{dom}R$$
12	5 11	eqsstrrid	$$⊢R\in \mathrm{DirRel}\to \bigcup \bigcup R\subseteq \mathrm{dom}R$$
13	4 12	eqssd	$$⊢R\in \mathrm{DirRel}\to \mathrm{dom}R=\bigcup \bigcup R$$