This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tospos

Description: A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018)

		Ref	Expression
	Assertion	tospos	$⊢ F \in Toset \to F \in Poset$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{F} = {Base}_{F}$
2		eqid	$⊢ \leq_{F} = \leq_{F}$
3	1 2	istos	$⊢ F \in Toset \leftrightarrow (F \in Poset \land \forall x \in {Base}_{F} \forall y \in {Base}_{F} (x \leq_{F} y \lor y \leq_{F} x))$
4	3	simplbi	$⊢ F \in Toset \to F \in Poset$