Theorem 2ndrn

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

	Ref	Expression
Assertion	2ndrn	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to 2^{nd}\left(A\right)\in \mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		simpr	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to A\in R$$
3	1 2	eqeltrrd	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in R$$
4		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
5		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
6	4 5	opelrn	$$⊢⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in R\to 2^{nd}\left(A\right)\in \mathrm{ran}R$$
7	3 6	syl	$$⊢\left(\mathrm{Rel}R\wedge A\in R\right)\to 2^{nd}\left(A\right)\in \mathrm{ran}R$$