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	⊢ ¬ 𝐴 < 𝐴

Proof

Step	Hyp	Ref	Expression
1		xrltnr	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )
2		opelxp1	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( ℝ* × ℝ* ) → 𝐴 ∈ ℝ* )
3	2	con3i	⊢ ( ¬ 𝐴 ∈ ℝ* → ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ ( ℝ* × ℝ* ) )
4		ltrelxr	⊢ < ⊆ ( ℝ* × ℝ* )
5	4	sseli	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ < → ⟨ 𝐴 , 𝐴 ⟩ ∈ ( ℝ* × ℝ* ) )
6	3 5	nsyl	⊢ ( ¬ 𝐴 ∈ ℝ* → ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ < )
7		df-br	⊢ ( 𝐴 < 𝐴 ↔ ⟨ 𝐴 , 𝐴 ⟩ ∈ < )
8	6 7	sylnibr	⊢ ( ¬ 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )
9	1 8	pm2.61i	⊢ ¬ 𝐴 < 𝐴