Theorem xrltso

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

	Ref	Expression
Assertion	xrltso	⊢ < Or ℝ*

Proof

Step	Hyp	Ref	Expression
1		xrlttri	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ¬ ( 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) )
2		xrlttr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 < 𝑦 ∧ 𝑦 < 𝑧 ) → 𝑥 < 𝑧 ) )
3	1 2	isso2i	⊢ < Or ℝ*