This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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