Description: The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | sum2id | ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumeq2ii | ⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) ) | |
2 | fvex | ⊢ ( I ‘ 𝐵 ) ∈ V | |
3 | fvi | ⊢ ( ( I ‘ 𝐵 ) ∈ V → ( I ‘ ( I ‘ 𝐵 ) ) = ( I ‘ 𝐵 ) ) | |
4 | 2 3 | ax-mp | ⊢ ( I ‘ ( I ‘ 𝐵 ) ) = ( I ‘ 𝐵 ) |
5 | 4 | eqcomi | ⊢ ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) ) |
6 | 5 | a1i | ⊢ ( 𝑘 ∈ 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ ( I ‘ 𝐵 ) ) ) |
7 | 1 6 | mprg | ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) |