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

Metamath Proof Explorer

Theorem sopo

Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997)

		Ref	Expression
	Assertion	sopo	$⊢ R Or A \to R Po A$

Step	Hyp	Ref	Expression
1		df-so	$⊢ R Or A \leftrightarrow (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
2	1	simplbi	$⊢ R Or A \to R Po A$