Metamath Proof Explorer

Theorem sdomnsym

Description: Strict dominance is asymmetric. Theorem 21(ii) of Suppes p. 97. (Contributed by NM, 8-Jun-1998)

Ref Expression
Assertion sdomnsym 
|- ( A ~< B -> -. B ~< A )

Proof

Step Hyp Ref Expression
1 sdomnen 
 |-  ( A ~< B -> -. A ~~ B )
2 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
3 sdomdom 
 |-  ( B ~< A -> B ~<_ A )
4 sbth 
 |-  ( ( A ~<_ B /\ B ~<_ A ) -> A ~~ B )
5 2 3 4 syl2an 
 |-  ( ( A ~< B /\ B ~< A ) -> A ~~ B )
6 1 5 mtand 
 |-  ( A ~< B -> -. B ~< A )