Metamath Proof Explorer

Theorem sge0pnffigtmpt

Description: If the generalized sum of nonnegative reals is +oo , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0pnffigtmpt.k ⊢ Ⅎ k φ
sge0pnffigtmpt.a ⊢ φ → A ∈ V
sge0pnffigtmpt.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
sge0pnffigtmpt.p ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = +∞
sge0pnffigtmpt.y ⊢ φ → Y ∈ ℝ
Assertion sge0pnffigtmpt ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ x ⟼ B

Proof

Step Hyp Ref Expression
1 sge0pnffigtmpt.k ⊢ Ⅎ k φ
2 sge0pnffigtmpt.a ⊢ φ → A ∈ V
3 sge0pnffigtmpt.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
4 sge0pnffigtmpt.p ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = +∞
5 sge0pnffigtmpt.y ⊢ φ → Y ∈ ℝ
6 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
7 1 3 6 fmptdf ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
8 2 7 4 5 sge0pnffigt ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ A ⟼ B ↾ x
9 simpr ⊢ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → Y < sum^ ⁡ k ∈ A ⟼ B ↾ x
10 elpwinss ⊢ x ∈ 𝒫 A ∩ Fin → x ⊆ A
11 10 adantr ⊢ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → x ⊆ A
12 11 resmptd ⊢ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → k ∈ A ⟼ B ↾ x = k ∈ x ⟼ B
13 12 fveq2d ⊢ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → sum^ ⁡ k ∈ A ⟼ B ↾ x = sum^ ⁡ k ∈ x ⟼ B
14 9 13 breqtrd ⊢ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → Y < sum^ ⁡ k ∈ x ⟼ B
15 14 ex ⊢ x ∈ 𝒫 A ∩ Fin → Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → Y < sum^ ⁡ k ∈ x ⟼ B
16 15 adantl ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → Y < sum^ ⁡ k ∈ x ⟼ B
17 16 reximdva ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ A ⟼ B ↾ x → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ x ⟼ B
18 8 17 mpd ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ x ⟼ B