Theorem fge0iccre

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

	Ref	Expression
Hypotheses	fge0iccre.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	fge0iccre.2	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
Assertion	fge0iccre	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		fge0iccre.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
2		fge0iccre.2	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
3	1 2	fge0iccico	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
4		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
5	4	a1i	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ℝ )
6	3 5	fssd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )