Theorem fge0iccico

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

	Ref	Expression
Hypotheses	fge0iccico.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	fge0iccico.re	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
Assertion	fge0iccico	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		fge0iccico.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
2		fge0iccico.re	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
3	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
4		0xr	⊢ 0 ∈ ℝ*
5	4	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ* )
6		pnfxr	⊢ +∞ ∈ ℝ*
7	6	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → +∞ ∈ ℝ* )
8		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
9	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
10	8 9	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
11		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
12	5 7 9 11	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
13	10	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
14		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ¬ ( 𝐹 ‘ 𝑥 ) < +∞ )
15	6	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → +∞ ∈ ℝ* )
16	15 13	xrlenltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ( +∞ ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) )
17	14 16	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → +∞ ≤ ( 𝐹 ‘ 𝑥 ) )
18	13 17	xrgepnfd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ( 𝐹 ‘ 𝑥 ) = +∞ )
19	18	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → +∞ = ( 𝐹 ‘ 𝑥 ) )
20	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Fun 𝐹 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
23		fdm	⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → dom 𝐹 = 𝑋 )
24	23	eqcomd	⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → 𝑋 = dom 𝐹 )
25	1 24	syl	⊢ ( 𝜑 → 𝑋 = dom 𝐹 )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 = dom 𝐹 )
27	22 26	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom 𝐹 )
28		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
29	21 27 28	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
31	19 30	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → +∞ ∈ ran 𝐹 )
32	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < +∞ ) → ¬ +∞ ∈ ran 𝐹 )
33	31 32	condan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) < +∞ )
34	5 7 10 12 33	elicod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
35	34	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
36	3 35	jca	⊢ ( 𝜑 → ( 𝐹 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
37		ffnfv	⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
38	36 37	sylibr	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )