Description: Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfesum1.1 | ⊢ Ⅎ 𝑘 𝐴 | |
Assertion | nfesum1 | ⊢ Ⅎ 𝑘 Σ* 𝑘 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfesum1.1 | ⊢ Ⅎ 𝑘 𝐴 | |
2 | df-esum | ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) | |
3 | nfcv | ⊢ Ⅎ 𝑘 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) | |
4 | nfcv | ⊢ Ⅎ 𝑘 tsums | |
5 | nfmpt1 | ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) | |
6 | 3 4 5 | nfov | ⊢ Ⅎ 𝑘 ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
7 | 6 | nfuni | ⊢ Ⅎ 𝑘 ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
8 | 2 7 | nfcxfr | ⊢ Ⅎ 𝑘 Σ* 𝑘 ∈ 𝐴 𝐵 |