Metamath Proof Explorer

Theorem sge0pnffigt

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

Ref Expression
Hypotheses sge0pnffigt.x ⊢ φ → X ∈ V
sge0pnffigt.f ⊢ φ → F : X ⟶ 0 +∞
sge0pnffigt.pnf ⊢ φ → sum^ ⁡ F = +∞
sge0pnffigt.y ⊢ φ → Y ∈ ℝ
Assertion sge0pnffigt ⊢ φ → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x

Proof

Step Hyp Ref Expression
1 sge0pnffigt.x ⊢ φ → X ∈ V
2 sge0pnffigt.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0pnffigt.pnf ⊢ φ → sum^ ⁡ F = +∞
4 sge0pnffigt.y ⊢ φ → Y ∈ ℝ
5 1 2 sge0sup ⊢ φ → sum^ ⁡ F = sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ℝ * <
6 5 3 eqtr3d ⊢ φ → sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ℝ * < = +∞
7 vex ⊢ x ∈ V
8 7 a1i ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ∈ V
9 2 adantr ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F : X ⟶ 0 +∞
10 elpwinss ⊢ x ∈ 𝒫 X ∩ Fin → x ⊆ X
11 10 adantl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → x ⊆ X
12 9 11 fssresd ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → F ↾ x : x ⟶ 0 +∞
13 8 12 sge0xrcl ⊢ φ ∧ x ∈ 𝒫 X ∩ Fin → sum^ ⁡ F ↾ x ∈ ℝ *
14 13 ralrimiva ⊢ φ → ∀ x ∈ 𝒫 X ∩ Fin sum^ ⁡ F ↾ x ∈ ℝ *
15 eqid ⊢ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x = x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x
16 15 rnmptss ⊢ ∀ x ∈ 𝒫 X ∩ Fin sum^ ⁡ F ↾ x ∈ ℝ * → ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ⊆ ℝ *
17 14 16 syl ⊢ φ → ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ⊆ ℝ *
18 supxrunb2 ⊢ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ⊆ ℝ * → ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x y < z ↔ sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ℝ * < = +∞
19 17 18 syl ⊢ φ → ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x y < z ↔ sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ℝ * < = +∞
20 6 19 mpbird ⊢ φ → ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x y < z
21 breq1 ⊢ y = Y → y < z ↔ Y < z
22 21 rexbidv ⊢ y = Y → ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x y < z ↔ ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x Y < z
23 22 rspcva ⊢ Y ∈ ℝ ∧ ∀ y ∈ ℝ ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x y < z → ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x Y < z
24 4 20 23 syl2anc ⊢ φ → ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x Y < z
25 vex ⊢ z ∈ V
26 15 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ↔ ∃ x ∈ 𝒫 X ∩ Fin z = sum^ ⁡ F ↾ x
27 25 26 ax-mp ⊢ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ↔ ∃ x ∈ 𝒫 X ∩ Fin z = sum^ ⁡ F ↾ x
28 27 biimpi ⊢ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x → ∃ x ∈ 𝒫 X ∩ Fin z = sum^ ⁡ F ↾ x
29 28 3ad2ant2 ⊢ φ ∧ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ∧ Y < z → ∃ x ∈ 𝒫 X ∩ Fin z = sum^ ⁡ F ↾ x
30 nfv ⊢ Ⅎ x φ
31 nfcv ⊢ Ⅎ _ x z
32 nfmpt1 ⊢ Ⅎ _ x x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x
33 32 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x
34 31 33 nfel ⊢ Ⅎ x z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x
35 nfv ⊢ Ⅎ x Y < z
36 30 34 35 nf3an ⊢ Ⅎ x φ ∧ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ∧ Y < z
37 simpl ⊢ Y < z ∧ z = sum^ ⁡ F ↾ x → Y < z
38 simpr ⊢ Y < z ∧ z = sum^ ⁡ F ↾ x → z = sum^ ⁡ F ↾ x
39 38 breq2d ⊢ Y < z ∧ z = sum^ ⁡ F ↾ x → Y < z ↔ Y < sum^ ⁡ F ↾ x
40 37 39 mpbid ⊢ Y < z ∧ z = sum^ ⁡ F ↾ x → Y < sum^ ⁡ F ↾ x
41 40 ex ⊢ Y < z → z = sum^ ⁡ F ↾ x → Y < sum^ ⁡ F ↾ x
42 41 adantl ⊢ φ ∧ Y < z → z = sum^ ⁡ F ↾ x → Y < sum^ ⁡ F ↾ x
43 42 a1d ⊢ φ ∧ Y < z → x ∈ 𝒫 X ∩ Fin → z = sum^ ⁡ F ↾ x → Y < sum^ ⁡ F ↾ x
44 43 3adant2 ⊢ φ ∧ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ∧ Y < z → x ∈ 𝒫 X ∩ Fin → z = sum^ ⁡ F ↾ x → Y < sum^ ⁡ F ↾ x
45 36 44 reximdai ⊢ φ ∧ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ∧ Y < z → ∃ x ∈ 𝒫 X ∩ Fin z = sum^ ⁡ F ↾ x → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x
46 29 45 mpd ⊢ φ ∧ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x ∧ Y < z → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x
47 46 3exp ⊢ φ → z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x → Y < z → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x
48 47 rexlimdv ⊢ φ → ∃ z ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ sum^ ⁡ F ↾ x Y < z → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x
49 24 48 mpd ⊢ φ → ∃ x ∈ 𝒫 X ∩ Fin Y < sum^ ⁡ F ↾ x