Metamath Proof Explorer

Theorem lern

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

Ref Expression
Assertion lern 
|- RR* = ran <_

Proof

Step Hyp Ref Expression
1 xrleid 
 |-  ( x e. RR* -> x <_ x )
2 lerel 
 |-  Rel <_
3 2 relelrni 
 |-  ( x <_ x -> x e. ran <_ )
4 1 3 syl 
 |-  ( x e. RR* -> x e. ran <_ )
5 4 ssriv 
 |-  RR* C_ ran <_
6 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
7 6 rnssi 
 |-  ran <_ C_ ran ( RR* X. RR* )
8 rnxpss 
 |-  ran ( RR* X. RR* ) C_ RR*
9 7 8 sstri 
 |-  ran <_ C_ RR*
10 5 9 eqssi 
 |-  RR* = ran <_