Metamath Proof Explorer

Theorem ledm

Description: The domain of <_ is RR* . (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 4-May-2015)

Ref Expression
Assertion ledm 
|- RR* = dom <_

Proof

Step Hyp Ref Expression
1 xrleid 
 |-  ( x e. RR* -> x <_ x )
2 lerel 
 |-  Rel <_
3 2 releldmi 
 |-  ( x <_ x -> x e. dom <_ )
4 1 3 syl 
 |-  ( x e. RR* -> x e. dom <_ )
5 4 ssriv 
 |-  RR* C_ dom <_
6 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
7 dmss 
 |-  ( <_ C_ ( RR* X. RR* ) -> dom <_ C_ dom ( RR* X. RR* ) )
8 6 7 ax-mp 
 |-  dom <_ C_ dom ( RR* X. RR* )
9 dmxpss 
 |-  dom ( RR* X. RR* ) C_ RR*
10 8 9 sstri 
 |-  dom <_ C_ RR*
11 5 10 eqssi 
 |-  RR* = dom <_