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 
|- ( ph -> X e. V )
sge0pnffigt.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0pnffigt.pnf 
|- ( ph -> ( sum^ ` F ) = +oo )
sge0pnffigt.y 
|- ( ph -> Y e. RR )
Assertion sge0pnffigt 
|- ( ph -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) )

Proof

Step Hyp Ref Expression
1 sge0pnffigt.x 
 |-  ( ph -> X e. V )
2 sge0pnffigt.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0pnffigt.pnf 
 |-  ( ph -> ( sum^ ` F ) = +oo )
4 sge0pnffigt.y 
 |-  ( ph -> Y e. RR )
5 1 2 sge0sup 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )
6 5 3 eqtr3d 
 |-  ( ph -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = +oo )
7 vex 
 |-  x e. _V
8 7 a1i 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. _V )
9 2 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
10 elpwinss 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
11 10 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
12 9 11 fssresd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
13 8 12 sge0xrcl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) e. RR* )
14 13 ralrimiva 
 |-  ( ph -> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* )
15 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) = ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
16 15 rnmptss 
 |-  ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
17 14 16 syl 
 |-  ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
18 supxrunb2 
 |-  ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* -> ( A. y e. RR E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y < z <-> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = +oo ) )
19 17 18 syl 
 |-  ( ph -> ( A. y e. RR E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y < z <-> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = +oo ) )
20 6 19 mpbird 
 |-  ( ph -> A. y e. RR E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y < z )
21 breq1 
 |-  ( y = Y -> ( y < z <-> Y < z ) )
22 21 rexbidv 
 |-  ( y = Y -> ( E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y < z <-> E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) Y < z ) )
23 22 rspcva 
 |-  ( ( Y e. RR /\ A. y e. RR E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) y < z ) -> E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) Y < z )
24 4 20 23 syl2anc 
 |-  ( ph -> E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) Y < z )
25 vex 
 |-  z e. _V
26 15 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) z = ( sum^ ` ( F |` x ) ) ) )
27 25 26 ax-mp 
 |-  ( z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) <-> E. x e. ( ~P X i^i Fin ) z = ( sum^ ` ( F |` x ) ) )
28 27 biimpi 
 |-  ( z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) -> E. x e. ( ~P X i^i Fin ) z = ( sum^ ` ( F |` x ) ) )
29 28 3ad2ant2 
 |-  ( ( ph /\ z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) /\ Y < z ) -> E. x e. ( ~P X i^i Fin ) z = ( sum^ ` ( F |` x ) ) )
30 nfv 
 |-  F/ x ph
31 nfcv 
 |-  F/_ x z
32 nfmpt1 
 |-  F/_ x ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
33 32 nfrn 
 |-  F/_ x ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
34 31 33 nfel 
 |-  F/ x z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
35 nfv 
 |-  F/ x Y < z
36 30 34 35 nf3an 
 |-  F/ x ( ph /\ z e. ran ( x e. ( ~P X i^i 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 
 |-  ( ( ph /\ Y < z ) -> ( z = ( sum^ ` ( F |` x ) ) -> Y < ( sum^ ` ( F |` x ) ) ) )
43 42 a1d 
 |-  ( ( ph /\ Y < z ) -> ( x e. ( ~P X i^i Fin ) -> ( z = ( sum^ ` ( F |` x ) ) -> Y < ( sum^ ` ( F |` x ) ) ) ) )
44 43 3adant2 
 |-  ( ( ph /\ z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) /\ Y < z ) -> ( x e. ( ~P X i^i Fin ) -> ( z = ( sum^ ` ( F |` x ) ) -> Y < ( sum^ ` ( F |` x ) ) ) ) )
45 36 44 reximdai 
 |-  ( ( ph /\ z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) /\ Y < z ) -> ( E. x e. ( ~P X i^i Fin ) z = ( sum^ ` ( F |` x ) ) -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) ) )
46 29 45 mpd 
 |-  ( ( ph /\ z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) /\ Y < z ) -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) )
47 46 3exp 
 |-  ( ph -> ( z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) -> ( Y < z -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) ) ) )
48 47 rexlimdv 
 |-  ( ph -> ( E. z e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) Y < z -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) ) )
49 24 48 mpd 
 |-  ( ph -> E. x e. ( ~P X i^i Fin ) Y < ( sum^ ` ( F |` x ) ) )