Metamath Proof Explorer

Theorem sumex

Description: A sum is a set. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumex ⊢ ∑ k ∈ A B ∈ V

Proof

Step Hyp Ref Expression
1 df-sum ⊢ ∑ k ∈ A B = ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
2 iotaex ⊢ ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ seq m + n ∈ ℤ ⟼ if n ∈ A ⦋ n / k⦌ B 0 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 + n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m ∈ V
3 1 2 eqeltri ⊢ ∑ k ∈ A B ∈ V