Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Extensible Structures
Posets
tospos
Next ⟩
resspos
Metamath Proof Explorer
Ascii
Unicode
Theorem
tospos
Description:
A Toset is a Poset.
(Contributed by
Thierry Arnoux
, 20-Jan-2018)
Ref
Expression
Assertion
tospos
⊢
F
∈
Toset
→
F
∈
Poset
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
Base
F
=
Base
F
2
eqid
⊢
≤
F
=
≤
F
3
1
2
istos
⊢
F
∈
Toset
↔
F
∈
Poset
∧
∀
x
∈
Base
F
∀
y
∈
Base
F
x
≤
F
y
∨
y
≤
F
x
4
3
simplbi
⊢
F
∈
Toset
→
F
∈
Poset