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	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
Assertion	fge0npnf	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fge0npnf.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
2	1	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,) +∞ ) )
3	2	adantr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ran 𝐹 ⊆ ( 0 [,) +∞ ) )
4		simpr	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ran 𝐹 )
5	3 4	sseldd	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → +∞ ∈ ( 0 [,) +∞ ) )
6		0xr	⊢ 0 ∈ ℝ*
7		icoub	⊢ ( 0 ∈ ℝ* → ¬ +∞ ∈ ( 0 [,) +∞ ) )
8	6 7	ax-mp	⊢ ¬ +∞ ∈ ( 0 [,) +∞ )
9	8	a1i	⊢ ( ( 𝜑 ∧ +∞ ∈ ran 𝐹 ) → ¬ +∞ ∈ ( 0 [,) +∞ ) )
10	5 9	pm2.65da	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )