Theorem fge0iccre

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

	Ref	Expression
Hypotheses	fge0iccre.1	|- ( ph -> F : X --> ( 0 [,] +oo ) )
	fge0iccre.2	|- ( ph -> -. +oo e. ran F )
Assertion	fge0iccre	|- ( ph -> F : X --> RR )

Proof

Step	Hyp	Ref	Expression
1		fge0iccre.1	|- ( ph -> F : X --> ( 0 [,] +oo ) )
2		fge0iccre.2	|- ( ph -> -. +oo e. ran F )
3	1 2	fge0iccico	|- ( ph -> F : X --> ( 0 [,) +oo ) )
4		rge0ssre	|- ( 0 [,) +oo ) C_ RR
5	4	a1i	|- ( ph -> ( 0 [,) +oo ) C_ RR )
6	3 5	fssd	|- ( ph -> F : X --> RR )