Theorem xrge0le

Description: The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018)

	Ref	Expression
Assertion	xrge0le	$$⊢\le ={\le }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$$
2		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
3		xrsle	$$⊢\le ={\le }_{{ℝ}_{𝑠}^{*}}$$
4	2 3	ressle	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}\to \le ={\le }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
5	1 4	ax-mp	$$⊢\le ={\le }_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$