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 +∞