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

Metamath Proof Explorer

Theorem xrltso

Description: 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005)

		Ref	Expression
	Assertion	xrltso	$⊢ < Or ℝ^{*}$

Step	Hyp	Ref	Expression
1		xrlttri	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \leftrightarrow \neg (x = y \lor y < x))$
2		xrlttr	$⊢ (x \in ℝ^{} \land y \in ℝ^{} \land z \in ℝ^{*}) \to ((x < y \land y < z) \to x < z)$
3	1 2	isso2i	$⊢ < Or ℝ^{*}$