Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets and lattices as relations
pstr2
Next ⟩
pslem
Metamath Proof Explorer
Ascii
Unicode
Theorem
pstr2
Description:
A poset is transitive.
(Contributed by
FL
, 3-Aug-2009)
Ref
Expression
Assertion
pstr2
⊢
R
∈
PosetRel
→
R
∘
R
⊆
R
Proof
Step
Hyp
Ref
Expression
1
isps
⊢
R
∈
PosetRel
→
R
∈
PosetRel
↔
Rel
⁡
R
∧
R
∘
R
⊆
R
∧
R
∩
R
-1
=
I
↾
⋃
⋃
R
2
1
ibi
⊢
R
∈
PosetRel
→
Rel
⁡
R
∧
R
∘
R
⊆
R
∧
R
∩
R
-1
=
I
↾
⋃
⋃
R
3
2
simp2d
⊢
R
∈
PosetRel
→
R
∘
R
⊆
R