Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets
postr
Next ⟩
0pos
Metamath Proof Explorer
Ascii
Unicode
Theorem
postr
Description:
A poset ordering is transitive.
(Contributed by
NM
, 11-Sep-2011)
Ref
Expression
Hypotheses
posi.b
⊢
B
=
Base
K
posi.l
⊢
≤
˙
=
≤
K
Assertion
postr
⊢
K
∈
Poset
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
≤
˙
Y
∧
Y
≤
˙
Z
→
X
≤
˙
Z
Proof
Step
Hyp
Ref
Expression
1
posi.b
⊢
B
=
Base
K
2
posi.l
⊢
≤
˙
=
≤
K
3
1
2
posi
⊢
K
∈
Poset
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
≤
˙
X
∧
X
≤
˙
Y
∧
Y
≤
˙
X
→
X
=
Y
∧
X
≤
˙
Y
∧
Y
≤
˙
Z
→
X
≤
˙
Z
4
3
simp3d
⊢
K
∈
Poset
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
≤
˙
Y
∧
Y
≤
˙
Z
→
X
≤
˙
Z