Metamath Proof Explorer

Theorem sge0rnbnd

Description: The range used in the definition of sum^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0rnbnd.x ⊢ φ → X ∈ V
sge0rnbnd.f ⊢ φ → F : X ⟶ 0 +∞
sge0rnbnd.re ⊢ φ → sum^ ⁡ F ∈ ℝ
Assertion sge0rnbnd ⊢ φ → ∃ z ∈ ℝ ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ z

Proof

Step Hyp Ref Expression
1 sge0rnbnd.x ⊢ φ → X ∈ V
2 sge0rnbnd.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0rnbnd.re ⊢ φ → sum^ ⁡ F ∈ ℝ
4 simpl ⊢ φ ∧ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → φ
5 vex ⊢ w ∈ V
6 eqid ⊢ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y = x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y
7 6 elrnmpt ⊢ w ∈ V → w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ↔ ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y
8 5 7 ax-mp ⊢ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ↔ ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y
9 8 biimpi ⊢ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y
10 9 adantl ⊢ φ ∧ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y
11 simp3 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → w = ∑ y ∈ x F ⁡ y
12 1 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → X ∈ V
13 2 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
14 1 2 3 sge0rern ⊢ φ → ¬ +∞ ∈ ran ⁡ F
15 14 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → ¬ +∞ ∈ ran ⁡ F
16 13 15 fge0iccico ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
17 elpwinss ⊢ x ∈ 𝒫 X ∩ Fin → x ⊆ X
18 17 adantl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ⊆ X
19 elinel2 ⊢ x ∈ 𝒫 X ∩ Fin → x ∈ Fin
20 19 adantl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ∈ Fin
21 12 16 18 20 fsumlesge0 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → ∑ y ∈ x F ⁡ y ≤ sum^ ⁡ F
22 21 3adant3 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → ∑ y ∈ x F ⁡ y ≤ sum^ ⁡ F
23 11 22 eqbrtrd ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
24 23 3exp ⊢ φ → x ∈ 𝒫 X ∩ Fin → w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
25 24 rexlimdv ⊢ φ → ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
26 4 10 25 sylc ⊢ φ ∧ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
27 26 ralrimiva ⊢ φ → ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ sum^ ⁡ F
28 brralrspcev ⊢ sum^ ⁡ F ∈ ℝ ∧ ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ sum^ ⁡ F → ∃ z ∈ ℝ ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ z
29 3 27 28 syl2anc ⊢ φ → ∃ z ∈ ℝ ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ z