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 * =

Proof

Step Hyp Ref Expression
1 lerel Rel ≤
2 relfld ( Rel ≤ → ≤ = ( dom ≤ ∪ ran ≤ ) )
3 1 2 ax-mp ≤ = ( dom ≤ ∪ ran ≤ )
4 ledm * = dom ≤
5 lern * = ran ≤
6 4 5 uneq12i ( ℝ* ∪ ℝ* ) = ( dom ≤ ∪ ran ≤ )
7 unidm ( ℝ* ∪ ℝ* ) = ℝ*
8 3 6 7 3eqtr2ri * =