Metamath Proof Explorer


Theorem fge0iccre

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

Ref Expression
Hypotheses fge0iccre.1 φ F : X 0 +∞
fge0iccre.2 φ ¬ +∞ ran F
Assertion fge0iccre φ F : X

Proof

Step Hyp Ref Expression
1 fge0iccre.1 φ F : X 0 +∞
2 fge0iccre.2 φ ¬ +∞ ran F
3 1 2 fge0iccico φ F : X 0 +∞
4 rge0ssre 0 +∞
5 4 a1i φ 0 +∞
6 3 5 fssd φ F : X