Theorem fge0npnf

Description: If F maps to nonnegative reals, then +oo is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	fge0npnf.1	|- ( ph -> F : X --> ( 0 [,) +oo ) )
Assertion	fge0npnf	|- ( ph -> -. +oo e. ran F )

Proof

Step	Hyp	Ref	Expression
1		fge0npnf.1	|- ( ph -> F : X --> ( 0 [,) +oo ) )
2	1	frnd	|- ( ph -> ran F C_ ( 0 [,) +oo ) )
3	2	adantr	|- ( ( ph /\ +oo e. ran F ) -> ran F C_ ( 0 [,) +oo ) )
4		simpr	|- ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
5	3 4	sseldd	|- ( ( ph /\ +oo e. ran F ) -> +oo e. ( 0 [,) +oo ) )
6		0xr	|- 0 e. RR*
7		icoub	|- ( 0 e. RR* -> -. +oo e. ( 0 [,) +oo ) )
8	6 7	ax-mp	|- -. +oo e. ( 0 [,) +oo )
9	8	a1i	|- ( ( ph /\ +oo e. ran F ) -> -. +oo e. ( 0 [,) +oo ) )
10	5 9	pm2.65da	|- ( ph -> -. +oo e. ran F )