Metamath Proof Explorer

Theorem dfsdom2

Description: Alternate definition of strict dominance. Compare Definition 3 of Suppes p. 97. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion dfsdom2 
|- ~< = ( ~<_ \ `' ~<_ )

Proof

Step Hyp Ref Expression
1 df-sdom 
 |-  ~< = ( ~<_ \ ~~ )
2 sbthcl 
 |-  ~~ = ( ~<_ i^i `' ~<_ )
3 2 difeq2i 
 |-  ( ~<_ \ ~~ ) = ( ~<_ \ ( ~<_ i^i `' ~<_ ) )
4 difin 
 |-  ( ~<_ \ ( ~<_ i^i `' ~<_ ) ) = ( ~<_ \ `' ~<_ )
5 1 3 4 3eqtri 
 |-  ~< = ( ~<_ \ `' ~<_ )