Theorem 1stdm

Description: The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	1stdm	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to 1^{st}\left(A\right)\in \mathrm{dom}R$$

Proof

Step	Hyp	Ref	Expression
1		df-rel	$$⊢\mathrm{Rel}R\leftrightarrow R\subseteq \mathrm{V}\times \mathrm{V}$$
2	1	biimpi	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{V}\times \mathrm{V}$$
3	2	sselda	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to A\in \left(\mathrm{V}\times \mathrm{V}\right)$$
4		1stval2	$$⊢A\in \left(\mathrm{V}\times \mathrm{V}\right)\to 1^{st}\left(A\right)=\bigcap \bigcap A$$
5	3 4	syl	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to 1^{st}\left(A\right)=\bigcap \bigcap A$$
6		elreldm	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to \bigcap \bigcap A\in \mathrm{dom}R$$
7	5 6	eqeltrd	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to 1^{st}\left(A\right)\in \mathrm{dom}R$$