Theorem xrltnsym2

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

	Ref	Expression
Assertion	xrltnsym2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \neg \left(A<B\wedge B<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltnsym	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\to \neg B<A\right)$$
2		imnan	$$⊢\left(A<B\to \neg B<A\right)\leftrightarrow \neg \left(A<B\wedge B<A\right)$$
3	1 2	sylib	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \neg \left(A<B\wedge B<A\right)$$