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	|- ( ph -> F : X --> ( 0 [,) +oo ) )
Assertion	fge0icoicc	|- ( ph -> F : X --> ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		fge0icoicc.1	|- ( ph -> F : X --> ( 0 [,) +oo ) )
2		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
3	2	a1i	|- ( ph -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
4	1 3	fssd	|- ( ph -> F : X --> ( 0 [,] +oo ) )