Database
BASIC ORDER THEORY
Posets, directed sets, and lattices as relations
Posets and lattices as relations
psrn
Next ⟩
psasym
Metamath Proof Explorer
Ascii
Unicode
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
syl5eq
⊢
R
∈
PosetRel
→
X
=
ran
⁡
R