Theorem fge0icoicc

Description: If F maps to nonnegative reals, then F maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	fge0icoicc.1	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right)$$
Assertion	fge0icoicc	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		fge0icoicc.1	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right)$$
2		icossicc	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$$
3	2	a1i	$$⊢\phi \to \left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$$
4	1 3	fssd	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$