Metamath Proof Explorer


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 𝑅 )