Metamath Proof Explorer


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 φ F : X 0 +∞
Assertion fge0icoicc φ F : X 0 +∞

Proof

Step Hyp Ref Expression
1 fge0icoicc.1 φ F : X 0 +∞
2 icossicc 0 +∞ 0 +∞
3 2 a1i φ 0 +∞ 0 +∞
4 1 3 fssd φ F : X 0 +∞