Theorem fge0iccre

Description: A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	fge0iccre.1	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
	fge0iccre.2	$$⊢\phi \to \neg \mathrm{+\infty }\in \mathrm{ran}F$$
Assertion	fge0iccre	$$⊢\phi \to F:X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		fge0iccre.1	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
2		fge0iccre.2	$$⊢\phi \to \neg \mathrm{+\infty }\in \mathrm{ran}F$$
3	1 2	fge0iccico	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right)$$
4		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
5	4	a1i	$$⊢\phi \to \left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
6	3 5	fssd	$$⊢\phi \to F:X⟶ℝ$$