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 ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		0elpw	⊢ ∅ ∈ 𝒫 𝑋
2		0fin	⊢ ∅ ∈ Fin
3	1 2	elini	⊢ ∅ ∈ ( 𝒫 𝑋 ∩ Fin )
4		sum0	⊢ Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) = 0
5	4	eqcomi	⊢ 0 = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 )
6		sumeq1	⊢ ( 𝑥 = ∅ → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) )
7	6	rspceeqv	⊢ ( ( ∅ ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 0 = Σ 𝑦 ∈ ∅ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
8	3 5 7	mp2an	⊢ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 )
9		0re	⊢ 0 ∈ ℝ
10		eqid	⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
11	10	elrnmpt	⊢ ( 0 ∈ ℝ → ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
12	9 11	ax-mp	⊢ ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
13	8 12	mpbir	⊢ 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
14		ne0i	⊢ ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
15	13 14	ax-mp	⊢ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ≠ ∅