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∈AB∈V

Proof

Step Hyp Ref Expression
1 df-sum ⊢∑k∈AB=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
2 iotaex ⊢ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m∈V
3 1 2 eqeltri ⊢∑k∈AB∈V