Metamath Proof Explorer

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 ⊢ φ → F : X ⟶ 0 +∞
Assertion fge0npnf ⊢ φ → ¬ +∞ ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 fge0npnf.1 ⊢ φ → F : X ⟶ 0 +∞
2 1 frnd ⊢ φ → ran ⁡ F ⊆ 0 +∞
3 2 adantr ⊢ φ ∧ +∞ ∈ ran ⁡ F → ran ⁡ F ⊆ 0 +∞
4 simpr ⊢ φ ∧ +∞ ∈ ran ⁡ F → +∞ ∈ ran ⁡ F
5 3 4 sseldd ⊢ φ ∧ +∞ ∈ ran ⁡ F → +∞ ∈ 0 +∞
6 0xr ⊢ 0 ∈ ℝ *
7 icoub ⊢ 0 ∈ ℝ * → ¬ +∞ ∈ 0 +∞
8 6 7 ax-mp ⊢ ¬ +∞ ∈ 0 +∞
9 8 a1i ⊢ φ ∧ +∞ ∈ ran ⁡ F → ¬ +∞ ∈ 0 +∞
10 5 9 pm2.65da ⊢ φ → ¬ +∞ ∈ ran ⁡ F