Theorem et-ltneverrefl

Description: Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024) Prefer to specify theorem domain and then apply ltnri . (New usage is discouraged.)

	Ref	Expression
Assertion	et-ltneverrefl	$$⊢\neg A<A$$

Proof

Step	Hyp	Ref	Expression
1		xrltnr	$$⊢A\in {ℝ}^{*}\to \neg A<A$$
2		opelxp1	$$⊢⟨A,A⟩\in \left({ℝ}^{*}\times {ℝ}^{*}\right)\to A\in {ℝ}^{*}$$
3	2	con3i	$$⊢\neg A\in {ℝ}^{*}\to \neg ⟨A,A⟩\in \left({ℝ}^{*}\times {ℝ}^{*}\right)$$
4		ltrelxr	$$⊢<\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
5	4	sseli	$$⊢⟨A,A⟩\in <\to ⟨A,A⟩\in \left({ℝ}^{*}\times {ℝ}^{*}\right)$$
6	3 5	nsyl	$$⊢\neg A\in {ℝ}^{*}\to \neg ⟨A,A⟩\in <$$
7		df-br	$$⊢A<A\leftrightarrow ⟨A,A⟩\in <$$
8	6 7	sylnibr	$$⊢\neg A\in {ℝ}^{*}\to \neg A<A$$
9	1 8	pm2.61i	$$⊢\neg A<A$$