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	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
Assertion	fge0icoicc	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		fge0icoicc.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
2		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
3	2	a1i	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
4	1 3	fssd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )