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	⊢ Ⅎ 𝑘 𝜑
	sge0pnffigtmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0pnffigtmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0pnffigtmpt.p	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
	sge0pnffigtmpt.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion	sge0pnffigtmpt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0pnffigtmpt.k	⊢ Ⅎ 𝑘 𝜑
2		sge0pnffigtmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0pnffigtmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0pnffigtmpt.p	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )
5		sge0pnffigtmpt.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
6		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
8	2 7 4 5	sge0pnffigt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) )
9		simpr	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) → 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) )
10		elpwinss	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ⊆ 𝐴 )
11	10	adantr	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) → 𝑥 ⊆ 𝐴 )
12	11	resmptd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) = ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) )
13	12	fveq2d	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) → ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
14	9 13	breqtrd	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) ) → 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
15	14	ex	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) → 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) → 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) )
17	16	reximdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝑥 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) )
18	8 17	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑌 < ( Σ^ ‘ ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )