Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets and lattices as relations
psrel
Next ⟩
psref2
Metamath Proof Explorer
Ascii
Unicode
Theorem
psrel
Description:
A poset is a relation.
(Contributed by
NM
, 12-May-2008)
Ref
Expression
Assertion
psrel
⊢
A
∈
PosetRel
→
Rel
⁡
A
Proof
Step
Hyp
Ref
Expression
1
isps
⊢
A
∈
PosetRel
→
A
∈
PosetRel
↔
Rel
⁡
A
∧
A
∘
A
⊆
A
∧
A
∩
A
-1
=
I
↾
⋃
⋃
A
2
1
ibi
⊢
A
∈
PosetRel
→
Rel
⁡
A
∧
A
∘
A
⊆
A
∧
A
∩
A
-1
=
I
↾
⋃
⋃
A
3
2
simp1d
⊢
A
∈
PosetRel
→
Rel
⁡
A