Description: A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | tospos | ⊢ ( 𝐹 ∈ Toset → 𝐹 ∈ Poset ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 ) | |
2 | eqid | ⊢ ( le ‘ 𝐹 ) = ( le ‘ 𝐹 ) | |
3 | 1 2 | istos | ⊢ ( 𝐹 ∈ Toset ↔ ( 𝐹 ∈ Poset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) ) |
4 | 3 | simplbi | ⊢ ( 𝐹 ∈ Toset → 𝐹 ∈ Poset ) |