Metamath Proof Explorer

Theorem sge0pnffsumgt

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

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

Proof

Step Hyp Ref Expression
1 sge0pnffsumgt.k ⊢ Ⅎ k φ
2 sge0pnffsumgt.a ⊢ φ → A ∈ V
3 sge0pnffsumgt.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
4 sge0pnffsumgt.p ⊢ φ → sum^ ⁡ k ∈ A ⟼ B = +∞
5 sge0pnffsumgt.y ⊢ φ → Y ∈ ℝ
6 icossicc ⊢ 0 +∞ ⊆ 0 +∞
7 6 3 sseldi ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
8 1 2 7 4 5 sge0pnffigtmpt ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ x ⟼ B
9 simpr ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ x ⟼ B → Y < sum^ ⁡ k ∈ x ⟼ B
10 nfv ⊢ Ⅎ k x ∈ 𝒫 A ∩ Fin
11 1 10 nfan ⊢ Ⅎ k φ ∧ x ∈ 𝒫 A ∩ Fin
12 elinel2 ⊢ x ∈ 𝒫 A ∩ Fin → x ∈ Fin
13 12 adantl ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → x ∈ Fin
14 simpll ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ k ∈ x → φ
15 elpwinss ⊢ x ∈ 𝒫 A ∩ Fin → x ⊆ A
16 15 sselda ⊢ x ∈ 𝒫 A ∩ Fin ∧ k ∈ x → k ∈ A
17 16 adantll ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ k ∈ x → k ∈ A
18 14 17 3 syl2anc ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ k ∈ x → B ∈ 0 +∞
19 11 13 18 sge0fsummptf ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → sum^ ⁡ k ∈ x ⟼ B = ∑ k ∈ x B
20 19 adantr ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ x ⟼ B → sum^ ⁡ k ∈ x ⟼ B = ∑ k ∈ x B
21 9 20 breqtrd ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin ∧ Y < sum^ ⁡ k ∈ x ⟼ B → Y < ∑ k ∈ x B
22 21 ex ⊢ φ ∧ x ∈ 𝒫 A ∩ Fin → Y < sum^ ⁡ k ∈ x ⟼ B → Y < ∑ k ∈ x B
23 22 reximdva ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < sum^ ⁡ k ∈ x ⟼ B → ∃ x ∈ 𝒫 A ∩ Fin Y < ∑ k ∈ x B
24 8 23 mpd ⊢ φ → ∃ x ∈ 𝒫 A ∩ Fin Y < ∑ k ∈ x B