Theorem xrge0base

Description: The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
2		df-ss	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\leftrightarrow \left[0,\mathrm{+\infty }\right]\cap {ℝ}^{*}=\left[0,\mathrm{+\infty }\right]$$
3	1 2	mpbi	$$⊢\left[0,\mathrm{+\infty }\right]\cap {ℝ}^{*}=\left[0,\mathrm{+\infty }\right]$$
4		ovex	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$$
5		eqid	$$⊢{ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]$$
6		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
7	5 6	ressbas	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}\to \left[0,\mathrm{+\infty }\right]\cap {ℝ}^{*}={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
8	4 7	ax-mp	$$⊢\left[0,\mathrm{+\infty }\right]\cap {ℝ}^{*}={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$
9	3 8	eqtr3i	$$⊢\left[0,\mathrm{+\infty }\right]={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$$