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	⊢ ℝ* = ∪ ∪ ≤