Theorem psrn

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

	Ref	Expression
Hypothesis	psref.1	⊢ 𝑋 = dom 𝑅
Assertion	psrn	⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		psref.1	⊢ 𝑋 = dom 𝑅
2		psdmrn	⊢ ( 𝑅 ∈ PosetRel → ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) )
3		eqtr3	⊢ ( ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) → dom 𝑅 = ran 𝑅 )
4	2 3	syl	⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ran 𝑅 )
5	1 4	syl5eq	⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 )