Theorem nfsum1

Description: Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

	Ref	Expression
Hypothesis	nfsum1.1	⊢ Ⅎ 𝑘 𝐴
Assertion	nfsum1	⊢ Ⅎ 𝑘 Σ 𝑘 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfsum1.1	⊢ Ⅎ 𝑘 𝐴
2		df-sum	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
3		nfcv	⊢ Ⅎ 𝑘 ℤ
4		nfcv	⊢ Ⅎ 𝑘 ( ℤ≥ ‘ 𝑚 )
5	1 4	nfss	⊢ Ⅎ 𝑘 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 )
6		nfcv	⊢ Ⅎ 𝑘 𝑚
7		nfcv	⊢ Ⅎ 𝑘 +
8	1	nfcri	⊢ Ⅎ 𝑘 𝑛 ∈ 𝐴
9		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵
10		nfcv	⊢ Ⅎ 𝑘 0
11	8 9 10	nfif	⊢ Ⅎ 𝑘 if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 )
12	3 11	nfmpt	⊢ Ⅎ 𝑘 ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
13	6 7 12	nfseq	⊢ Ⅎ 𝑘 seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) )
14		nfcv	⊢ Ⅎ 𝑘 ⇝
15		nfcv	⊢ Ⅎ 𝑘 𝑥
16	13 14 15	nfbr	⊢ Ⅎ 𝑘 seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥
17	5 16	nfan	⊢ Ⅎ 𝑘 ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 )
18	3 17	nfrex	⊢ Ⅎ 𝑘 ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 )
19		nfcv	⊢ Ⅎ 𝑘 ℕ
20		nfcv	⊢ Ⅎ 𝑘 𝑓
21		nfcv	⊢ Ⅎ 𝑘 ( 1 ... 𝑚 )
22	20 21 1	nff1o	⊢ Ⅎ 𝑘 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴
23		nfcv	⊢ Ⅎ 𝑘 1
24		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵
25	19 24	nfmpt	⊢ Ⅎ 𝑘 ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
26	23 7 25	nfseq	⊢ Ⅎ 𝑘 seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) )
27	26 6	nffv	⊢ Ⅎ 𝑘 ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
28	27	nfeq2	⊢ Ⅎ 𝑘 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
29	22 28	nfan	⊢ Ⅎ 𝑘 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
30	29	nfex	⊢ Ⅎ 𝑘 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
31	19 30	nfrex	⊢ Ⅎ 𝑘 ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
32	18 31	nfor	⊢ Ⅎ 𝑘 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
33	32	nfiotaw	⊢ Ⅎ 𝑘 ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
34	2 33	nfcxfr	⊢ Ⅎ 𝑘 Σ 𝑘 ∈ 𝐴 𝐵