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 e. RR* /\ B e. RR* ) -> -. ( A < B /\ B < A ) )

Proof

Step Hyp Ref Expression
1 xrltnsym 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -. B < A ) )
2 imnan 
 |-  ( ( A < B -> -. B < A ) <-> -. ( A < B /\ B < A ) )
3 1 2 sylib 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -. ( A < B /\ B < A ) )