fge0iccico

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

	Ref	Expression
Hypotheses	fge0iccico.f	$⊢ φ \to F : X ⟶ [0, +∞]$
	fge0iccico.re	$⊢ φ \to \neg +∞ \in ran F$
Assertion	fge0iccico	$⊢ φ \to F : X ⟶ [0, +∞)$

Proof

Step	Hyp	Ref	Expression
1		fge0iccico.f	$⊢ φ \to F : X ⟶ [0, +∞]$
2		fge0iccico.re	$⊢ φ \to \neg +∞ \in ran F$
3	1	ffnd	$⊢ φ \to F Fn X$
4		0xr	$⊢ 0 \in ℝ^{*}$
5	4	a1i	$⊢ (φ \land x \in X) \to 0 \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7	6	a1i	$⊢ (φ \land x \in X) \to +∞ \in ℝ^{*}$
8		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
9	1	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in [0, +∞]$
10	8 9	sselid	$⊢ (φ \land x \in X) \to F (x) \in ℝ^{*}$
11		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (x) \in [0, +∞]) \to 0 \leq F (x)$
12	5 7 9 11	syl3anc	$⊢ (φ \land x \in X) \to 0 \leq F (x)$
13	10	adantr	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to F (x) \in ℝ^{*}$
14		simpr	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to \neg F (x) < +∞$
15	6	a1i	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to +∞ \in ℝ^{*}$
16	15 13	xrlenltd	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to (+∞ \leq F (x) \leftrightarrow \neg F (x) < +∞)$
17	14 16	mpbird	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to +∞ \leq F (x)$
18	13 17	xrgepnfd	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to F (x) = +∞$
19	18	eqcomd	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to +∞ = F (x)$
20	1	ffund	$⊢ φ \to Fun F$
21	20	adantr	$⊢ (φ \land x \in X) \to Fun F$
22		simpr	$⊢ (φ \land x \in X) \to x \in X$
23		fdm	$⊢ F : X ⟶ [0, +∞] \to dom F = X$
24	23	eqcomd	$⊢ F : X ⟶ [0, +∞] \to X = dom F$
25	1 24	syl	$⊢ φ \to X = dom F$
26	25	adantr	$⊢ (φ \land x \in X) \to X = dom F$
27	22 26	eleqtrd	$⊢ (φ \land x \in X) \to x \in dom F$
28		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
29	21 27 28	syl2anc	$⊢ (φ \land x \in X) \to F (x) \in ran F$
30	29	adantr	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to F (x) \in ran F$
31	19 30	eqeltrd	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to +∞ \in ran F$
32	2	ad2antrr	$⊢ ((φ \land x \in X) \land \neg F (x) < +∞) \to \neg +∞ \in ran F$
33	31 32	condan	$⊢ (φ \land x \in X) \to F (x) < +∞$
34	5 7 10 12 33	elicod	$⊢ (φ \land x \in X) \to F (x) \in [0, +∞)$
35	34	ralrimiva	$⊢ φ \to \forall x \in X F (x) \in [0, +∞)$
36	3 35	jca	$⊢ φ \to (F Fn X \land \forall x \in X F (x) \in [0, +∞))$
37		ffnfv	$⊢ F : X ⟶ [0, +∞) \leftrightarrow (F Fn X \land \forall x \in X F (x) \in [0, +∞))$
38	36 37	sylibr	$⊢ φ \to F : X ⟶ [0, +∞)$

Metamath Proof Explorer

Theorem fge0iccico

Proof