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∈𝒫X∩Fin⟼∑y∈xF⁡y≠∅

Proof

Step Hyp Ref Expression
1 0elpw ⊢∅∈𝒫X
2 0fin ⊢∅∈Fin
3 1 2 elini ⊢∅∈𝒫X∩Fin
4 sum0 ⊢∑y∈∅F⁡y=0
5 4 eqcomi ⊢0=∑y∈∅F⁡y
6 sumeq1 ⊢x=∅→∑y∈xF⁡y=∑y∈∅F⁡y
7 6 rspceeqv ⊢∅∈𝒫X∩Fin∧0=∑y∈∅F⁡y→∃x∈𝒫X∩Fin0=∑y∈xF⁡y
8 3 5 7 mp2an ⊢∃x∈𝒫X∩Fin0=∑y∈xF⁡y
9 0re ⊢0∈ℝ
10 eqid ⊢x∈𝒫X∩Fin⟼∑y∈xF⁡y=x∈𝒫X∩Fin⟼∑y∈xF⁡y
11 10 elrnmpt ⊢0∈ℝ→0∈ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y↔∃x∈𝒫X∩Fin0=∑y∈xF⁡y
12 9 11 ax-mp ⊢0∈ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y↔∃x∈𝒫X∩Fin0=∑y∈xF⁡y
13 8 12 mpbir ⊢0∈ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y
14 ne0i ⊢0∈ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y→ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y≠∅
15 13 14 ax-mp ⊢ran⁡x∈𝒫X∩Fin⟼∑y∈xF⁡y≠∅