Theorem xrltso

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

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

Proof

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