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	$⊢ ℝ^{*} = ⋃ ⋃ \leq$

Proof

Step	Hyp	Ref	Expression
1		lerel	$⊢ Rel \leq$
2		relfld	$⊢ Rel \leq \to ⋃ ⋃ \leq = dom \leq \cup ran \leq$
3	1 2	ax-mp	$⊢ ⋃ ⋃ \leq = dom \leq \cup ran \leq$
4		ledm	$⊢ ℝ^{*} = dom \leq$
5		lern	$⊢ ℝ^{*} = ran \leq$
6	4 5	uneq12i	$⊢ ℝ^{} \cup ℝ^{} = dom \leq \cup ran \leq$
7		unidm	$⊢ ℝ^{} \cup ℝ^{} = ℝ^{*}$
8	3 6 7	3eqtr2ri	$⊢ ℝ^{*} = ⋃ ⋃ \leq$