This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-sdom

Description: Define the strict dominance relation. Alternate possible definitions are derived as brsdom and brsdom2 . Definition 3 of Suppes p. 97. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion df-sdom 
|- ~< = ( ~<_ \ ~~ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csdm 
 |-  ~<
1 cdom 
 |-  ~<_
2 cen 
 |-  ~~
3 1 2 cdif 
 |-  ( ~<_ \ ~~ )
4 0 3 wceq 
 |-  ~< = ( ~<_ \ ~~ )