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

Metamath Proof Explorer

Theorem ltso

Description: 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997)

		Ref	Expression
	Assertion	ltso	$⊢ < Or ℝ$

Step	Hyp	Ref	Expression
1		axlttri	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow \neg (x = y \lor y < x))$
2		lttr	$⊢ (x \in ℝ \land y \in ℝ \land z \in ℝ) \to ((x < y \land y < z) \to x < z)$
3	1 2	isso2i	$⊢ < Or ℝ$