Metamath Proof Explorer

Theorem sdomirr

Description: Strict dominance is irreflexive. Theorem 21(i) of Suppes p. 97. (Contributed by NM, 4-Jun-1998)

Ref Expression
Assertion sdomirr 
|- -. A ~< A

Proof

Step Hyp Ref Expression
1 sdomnen 
 |-  ( A ~< A -> -. A ~~ A )
2 enrefg 
 |-  ( A e. _V -> A ~~ A )
3 1 2 nsyl3 
 |-  ( A e. _V -> -. A ~< A )
4 relsdom 
 |-  Rel ~<
5 4 brrelex1i 
 |-  ( A ~< A -> A e. _V )
6 5 con3i 
 |-  ( -. A e. _V -> -. A ~< A )
7 3 6 pm2.61i 
 |-  -. A ~< A