This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ X = dom ⁡ R
Assertion psrn ⊢ R ∈ PosetRel → X = ran ⁡ R

Proof

Step Hyp Ref Expression
1 psref.1 ⊢ X = dom ⁡ R
2 psdmrn ⊢ R ∈ PosetRel → dom ⁡ R = ⋃ ⋃ R ∧ ran ⁡ R = ⋃ ⋃ R
3 eqtr3 ⊢ dom ⁡ R = ⋃ ⋃ R ∧ ran ⁡ R = ⋃ ⋃ R → dom ⁡ R = ran ⁡ R
4 2 3 syl ⊢ R ∈ PosetRel → dom ⁡ R = ran ⁡ R
5 1 4 eqtrid ⊢ R ∈ PosetRel → X = ran ⁡ R