Metamath Proof Explorer

Theorem sge0rnn0

Description: The range used in the definition of sum^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion sge0rnn0 
|- ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)

Proof

Step Hyp Ref Expression
1 0elpw 
 |-  (/) e. ~P X
2 0fi 
 |-  (/) e. Fin
3 1 2 elini 
 |-  (/) e. ( ~P X i^i Fin )
4 sum0 
 |-  sum_ y e. (/) ( F ` y ) = 0
5 4 eqcomi 
 |-  0 = sum_ y e. (/) ( F ` y )
6 sumeq1 
 |-  ( x = (/) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
7 6 rspceeqv 
 |-  ( ( (/) e. ( ~P X i^i Fin ) /\ 0 = sum_ y e. (/) ( F ` y ) ) -> E. x e. ( ~P X i^i Fin ) 0 = sum_ y e. x ( F ` y ) )
8 3 5 7 mp2an 
 |-  E. x e. ( ~P X i^i Fin ) 0 = sum_ y e. x ( F ` y )
9 0re 
 |-  0 e. RR
10 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
11 10 elrnmpt 
 |-  ( 0 e. RR -> ( 0 e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) 0 = sum_ y e. x ( F ` y ) ) )
12 9 11 ax-mp 
 |-  ( 0 e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) 0 = sum_ y e. x ( F ` y ) )
13 8 12 mpbir 
 |-  0 e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
14 ne0i 
 |-  ( 0 e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/) )
15 13 14 ax-mp 
 |-  ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)