Theorem sge0rnre

Description: When sum^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	sge0rnre.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
Assertion	sge0rnre	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		sge0rnre.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
2		elinel2	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ Fin )
3	2	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ Fin )
4		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
5	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
6		elinel1	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑋 )
7		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
8	6 7	syl	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
9	8	adantr	⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑋 )
10		simpr	⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
11	9 10	sseldd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
12	11	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑋 )
13	5 12	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
14	4 13	sseldi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15	3 14	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
17		eqid	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
18	17	rnmptss	⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ℝ → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
19	16 18	syl	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )