Theorem ltnr

Description: 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999)

	Ref	Expression
Assertion	ltnr	$$⊢A\in ℝ\to \neg A<A$$

Proof

Step	Hyp	Ref	Expression
1		ltso	$$⊢<\mathrm{Or}ℝ$$
2		sonr	$$⊢\left(<\mathrm{Or}ℝ\wedge A\in ℝ\right)\to \neg A<A$$
3	1 2	mpan	$$⊢A\in ℝ\to \neg A<A$$