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∩FinY<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∩FinY<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∩FinY<sum^⁡k∈A⟼B↾x→∃x∈𝒫A∩FinY<sum^⁡k∈x⟼B
18 8 17 mpd ⊢φ→∃x∈𝒫A∩FinY<sum^⁡k∈x⟼B