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	\|- F/ k ph
		sge0pnffigtmpt.a	\|- ( ph -> A e. V )
		sge0pnffigtmpt.b	\|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
		sge0pnffigtmpt.p	\|- ( ph -> ( sum^ ` ( k e. A \|-> B ) ) = +oo )
		sge0pnffigtmpt.y	\|- ( ph -> Y e. RR )
	Assertion	sge0pnffigtmpt	\|- ( ph -> E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( k e. x \|-> B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0pnffigtmpt.k	\|- F/ k ph
2		sge0pnffigtmpt.a	\|- ( ph -> A e. V )
3		sge0pnffigtmpt.b	\|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4		sge0pnffigtmpt.p	\|- ( ph -> ( sum^ ` ( k e. A \|-> B ) ) = +oo )
5		sge0pnffigtmpt.y	\|- ( ph -> Y e. RR )
6		eqid	\|- ( k e. A \|-> B ) = ( k e. A \|-> B )
7	1 3 6	fmptdf	\|- ( ph -> ( k e. A \|-> B ) : A --> ( 0 [,] +oo ) )
8	2 7 4 5	sge0pnffigt	\|- ( ph -> E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) )
9		simpr	\|- ( ( x e. ( ~P A i^i Fin ) /\ Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) ) -> Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) )
10		elpwinss	\|- ( x e. ( ~P A i^i Fin ) -> x C_ A )
11	10	adantr	\|- ( ( x e. ( ~P A i^i Fin ) /\ Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) ) -> x C_ A )
12	11	resmptd	\|- ( ( x e. ( ~P A i^i Fin ) /\ Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) ) -> ( ( k e. A \|-> B ) \|` x ) = ( k e. x \|-> B ) )
13	12	fveq2d	\|- ( ( x e. ( ~P A i^i Fin ) /\ Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) ) -> ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) = ( sum^ ` ( k e. x \|-> B ) ) )
14	9 13	breqtrd	\|- ( ( x e. ( ~P A i^i Fin ) /\ Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) ) -> Y < ( sum^ ` ( k e. x \|-> B ) ) )
15	14	ex	\|- ( x e. ( ~P A i^i Fin ) -> ( Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) -> Y < ( sum^ ` ( k e. x \|-> B ) ) ) )
16	15	adantl	\|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) -> Y < ( sum^ ` ( k e. x \|-> B ) ) ) )
17	16	reximdva	\|- ( ph -> ( E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( ( k e. A \|-> B ) \|` x ) ) -> E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( k e. x \|-> B ) ) ) )
18	8 17	mpd	\|- ( ph -> E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( k e. x \|-> B ) ) )