Metamath Proof Explorer

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 ⊢Ⅎ_kA
Assertion nfsum1 ⊢Ⅎ_k∑k∈AB

Proof

Step Hyp Ref Expression
1 nfsum1.1 ⊢Ⅎ_kA
2 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
3 nfcv ⊢Ⅎ_kℤ
4 nfcv ⊢Ⅎ_kℤ≥m
5 1 4 nfss ⊢ℲkA⊆ℤ≥m
6 nfcv ⊢Ⅎ_km
7 nfcv ⊢Ⅎ_k+
8 1 nfcri ⊢Ⅎkn∈A
9 nfcsb1v ⊢Ⅎ_k⦋n/k⦌B
10 nfcv ⊢Ⅎ_k0
11 8 9 10 nfif ⊢Ⅎ_kifn∈A⦋n/k⦌B0
12 3 11 nfmpt ⊢Ⅎ_kn∈ℤ⟼ifn∈A⦋n/k⦌B0
13 6 7 12 nfseq ⊢Ⅎ_kseqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0
14 nfcv ⊢Ⅎ_k⇝
15 nfcv ⊢Ⅎ_kx
16 13 14 15 nfbr ⊢Ⅎkseqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
17 5 16 nfan ⊢ℲkA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
18 3 17 nfrexw ⊢Ⅎk∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
19 nfcv ⊢Ⅎ_kℕ
20 nfcv ⊢Ⅎ_kf
21 nfcv ⊢Ⅎ_k1…m
22 20 21 1 nff1o ⊢Ⅎkf:1…m⟶1-1 ontoA
23 nfcv ⊢Ⅎ_k1
24 nfcsb1v ⊢Ⅎ_k⦋f⁡n/k⦌B
25 19 24 nfmpt ⊢Ⅎ_kn∈ℕ⟼⦋f⁡n/k⦌B
26 23 7 25 nfseq ⊢Ⅎ_kseq1+n∈ℕ⟼⦋f⁡n/k⦌B
27 26 6 nffv ⊢Ⅎ_kseq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
28 27 nfeq2 ⊢Ⅎkx=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
29 22 28 nfan ⊢Ⅎkf:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
30 29 nfex ⊢Ⅎk∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
31 19 30 nfrexw ⊢Ⅎk∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
32 18 31 nfor ⊢Ⅎk∃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
33 32 nfiotaw ⊢Ⅎ_kι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
34 2 33 nfcxfr ⊢Ⅎ_k∑k∈AB