Metamath Proof Explorer

Theorem relsdom

Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion relsdom 
|- Rel ~<

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 reldif 
 |-  ( Rel ~<_ -> Rel ( ~<_ \ ~~ ) )
3 df-sdom 
 |-  ~< = ( ~<_ \ ~~ )
4 3 releqi 
 |-  ( Rel ~< <-> Rel ( ~<_ \ ~~ ) )
5 2 4 sylibr 
 |-  ( Rel ~<_ -> Rel ~< )
6 1 5 ax-mp 
 |-  Rel ~<