Theorem psrn

Description: The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008)

	Ref	Expression
Hypothesis	psref.1	$$⊢X=\mathrm{dom}R$$
Assertion	psrn	$$⊢R\in \mathrm{PosetRel}\to X=\mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		psref.1	$$⊢X=\mathrm{dom}R$$
2		psdmrn	$$⊢R\in \mathrm{PosetRel}\to \left(\mathrm{dom}R=\bigcup \bigcup R\wedge \mathrm{ran}R=\bigcup \bigcup R\right)$$
3		eqtr3	$$⊢\left(\mathrm{dom}R=\bigcup \bigcup R\wedge \mathrm{ran}R=\bigcup \bigcup R\right)\to \mathrm{dom}R=\mathrm{ran}R$$
4	2 3	syl	$$⊢R\in \mathrm{PosetRel}\to \mathrm{dom}R=\mathrm{ran}R$$
5	1 4	syl5eq	$$⊢R\in \mathrm{PosetRel}\to X=\mathrm{ran}R$$