Theorem psrn

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

	Ref	Expression
Hypothesis	psref.1	|- X = dom R
Assertion	psrn	|- ( R e. PosetRel -> X = ran R )

Proof

Step	Hyp	Ref	Expression
1		psref.1	|- X = dom R
2		psdmrn	|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )
3		eqtr3	|- ( ( dom R = U. U. R /\ ran R = U. U. R ) -> dom R = ran R )
4	2 3	syl	|- ( R e. PosetRel -> dom R = ran R )
5	1 4	eqtrid	|- ( R e. PosetRel -> X = ran R )