Metamath Proof Explorer

Theorem xrltnsym2

Description: 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion xrltnsym2 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ¬ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 xrltnsym ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
2 imnan ⊢ ( ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) ↔ ¬ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐴 ) )
3 1 2 sylib ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ¬ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐴 ) )