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 bilani ⊢ φ ∧ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y
10 simp3 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → w = ∑ y ∈ x F ⁡ y
11 1 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → X ∈ V
12 2 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
13 1 2 3 sge0rern ⊢ φ → ¬ +∞ ∈ ran ⁡ F
14 13 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → ¬ +∞ ∈ ran ⁡ F
15 12 14 fge0iccico ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
16 elpwinss ⊢ x ∈ 𝒫 X ∩ Fin → x ⊆ X
17 16 adantl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ⊆ X
18 elinel2 ⊢ x ∈ 𝒫 X ∩ Fin → x ∈ Fin
19 18 adantl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ∈ Fin
20 11 15 17 19 fsumlesge0 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → ∑ y ∈ x F ⁡ y ≤ sum^ ⁡ F
21 20 3adant3 ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → ∑ y ∈ x F ⁡ y ≤ sum^ ⁡ F
22 10 21 eqbrtrd ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin ∧ w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
23 22 3exp ⊢ φ → x ∈ 𝒫 X ∩ Fin → w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
24 23 rexlimdv ⊢ φ → ∃ x ∈ 𝒫 X ∩ Fin w = ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
25 4 9 24 sylc ⊢ φ ∧ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → w ≤ sum^ ⁡ F
26 25 ralrimiva ⊢ φ → ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ sum^ ⁡ F
27 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
28 3 26 27 syl2anc ⊢ φ → ∃ z ∈ ℝ ∀ w ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y w ≤ z