Theorem ltso

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

	Ref	Expression
Assertion	ltso	⊢ < Or ℝ

Proof

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