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 ∈ x F ⁡ 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 ∈ x F ⁡ y = ∑ y ∈ ∅ F ⁡ y
7 6 rspceeqv ⊢ ∅ ∈ 𝒫 X ∩ Fin ∧ 0 = ∑ y ∈ ∅ F ⁡ y → ∃ x ∈ 𝒫 X ∩ Fin 0 = ∑ y ∈ x F ⁡ y
8 3 5 7 mp2an ⊢ ∃ x ∈ 𝒫 X ∩ Fin 0 = ∑ y ∈ x F ⁡ y
9 0re ⊢ 0 ∈ ℝ
10 eqid ⊢ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y = x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y
11 10 elrnmpt ⊢ 0 ∈ ℝ → 0 ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ↔ ∃ x ∈ 𝒫 X ∩ Fin 0 = ∑ y ∈ x F ⁡ y
12 9 11 ax-mp ⊢ 0 ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ↔ ∃ x ∈ 𝒫 X ∩ Fin 0 = ∑ y ∈ x F ⁡ y
13 8 12 mpbir ⊢ 0 ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y
14 ne0i ⊢ 0 ∈ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y → ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ≠ ∅
15 13 14 ax-mp ⊢ ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ≠ ∅