Metamath Proof Explorer

Theorem domnsym

Description: Theorem 22(i) of Suppes p. 97. (Contributed by NM, 10-Jun-1998)

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

Proof

Step Hyp Ref Expression
1 brdom2 
 |-  ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
2 sdomnsym 
 |-  ( A ~< B -> -. B ~< A )
3 sdomnen 
 |-  ( B ~< A -> -. B ~~ A )
4 ensym 
 |-  ( A ~~ B -> B ~~ A )
5 3 4 nsyl3 
 |-  ( A ~~ B -> -. B ~< A )
6 2 5 jaoi 
 |-  ( ( A ~< B \/ A ~~ B ) -> -. B ~< A )
7 1 6 sylbi 
 |-  ( A ~<_ B -> -. B ~< A )