Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets and lattices as relations
psref
Next ⟩
psrn
Metamath Proof Explorer
Ascii
Unicode
Theorem
psref
Description:
A poset is reflexive.
(Contributed by
NM
, 13-May-2008)
Ref
Expression
Hypothesis
psref.1
⊢
X
=
dom
⁡
R
Assertion
psref
⊢
R
∈
PosetRel
∧
A
∈
X
→
A
R
A
Proof
Step
Hyp
Ref
Expression
1
psref.1
⊢
X
=
dom
⁡
R
2
psdmrn
⊢
R
∈
PosetRel
→
dom
⁡
R
=
⋃
⋃
R
∧
ran
⁡
R
=
⋃
⋃
R
3
2
simpld
⊢
R
∈
PosetRel
→
dom
⁡
R
=
⋃
⋃
R
4
1
3
syl5eq
⊢
R
∈
PosetRel
→
X
=
⋃
⋃
R
5
4
eleq2d
⊢
R
∈
PosetRel
→
A
∈
X
↔
A
∈
⋃
⋃
R
6
pslem
⊢
R
∈
PosetRel
→
A
R
A
∧
A
R
A
→
A
R
A
∧
A
∈
⋃
⋃
R
→
A
R
A
∧
A
R
A
∧
A
R
A
→
A
=
A
7
6
simp2d
⊢
R
∈
PosetRel
→
A
∈
⋃
⋃
R
→
A
R
A
8
5
7
sylbid
⊢
R
∈
PosetRel
→
A
∈
X
→
A
R
A
9
8
imp
⊢
R
∈
PosetRel
∧
A
∈
X
→
A
R
A