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

Proof

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