This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ A < B ∧ B < A

Proof

Step Hyp Ref Expression
1 xrltnsym ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B → ¬ B < A
2 imnan ⊢ A < B → ¬ B < A ↔ ¬ A < B ∧ B < A
3 1 2 sylib ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ A < B ∧ B < A