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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0pnffigt.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0pnffigt.pnf ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = +∞ )
sge0pnffigt.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion sge0pnffigt ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )

Proof

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