Metamath Proof Explorer

Theorem lefld

Description: The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 4-May-2015)

Ref Expression
Assertion lefld 
|- RR* = U. U. <_

Proof

Step Hyp Ref Expression
1 lerel 
 |-  Rel <_
2 relfld 
 |-  ( Rel <_ -> U. U. <_ = ( dom <_ u. ran <_ ) )
3 1 2 ax-mp 
 |-  U. U. <_ = ( dom <_ u. ran <_ )
4 ledm 
 |-  RR* = dom <_
5 lern 
 |-  RR* = ran <_
6 4 5 uneq12i 
 |-  ( RR* u. RR* ) = ( dom <_ u. ran <_ )
7 unidm 
 |-  ( RR* u. RR* ) = RR*
8 3 6 7 3eqtr2ri 
 |-  RR* = U. U. <_