Theorem nfcprod

Description: Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B , it is not free in prod_ k e. A B . (Contributed by Scott Fenton, 1-Dec-2017)

	Ref	Expression
Hypotheses	nfcprod.1	⊢ Ⅎ 𝑥 𝐴
	nfcprod.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfcprod	⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfcprod.1	⊢ Ⅎ 𝑥 𝐴
2		nfcprod.2	⊢ Ⅎ 𝑥 𝐵
3		df-prod	⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑦 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
4		nfcv	⊢ Ⅎ 𝑥 ℤ
5		nfcv	⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑚 )
6	1 5	nfss	⊢ Ⅎ 𝑥 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 )
7		nfv	⊢ Ⅎ 𝑥 𝑧 ≠ 0
8		nfcv	⊢ Ⅎ 𝑥 𝑛
9		nfcv	⊢ Ⅎ 𝑥 ·
10	1	nfcri	⊢ Ⅎ 𝑥 𝑘 ∈ 𝐴
11		nfcv	⊢ Ⅎ 𝑥 1
12	10 2 11	nfif	⊢ Ⅎ 𝑥 if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 )
13	4 12	nfmpt	⊢ Ⅎ 𝑥 ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
14	8 9 13	nfseq	⊢ Ⅎ 𝑥 seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) )
15		nfcv	⊢ Ⅎ 𝑥 ⇝
16		nfcv	⊢ Ⅎ 𝑥 𝑧
17	14 15 16	nfbr	⊢ Ⅎ 𝑥 seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧
18	7 17	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 )
19	18	nfex	⊢ Ⅎ 𝑥 ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 )
20	5 19	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 )
21		nfcv	⊢ Ⅎ 𝑥 𝑚
22	21 9 13	nfseq	⊢ Ⅎ 𝑥 seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) )
23		nfcv	⊢ Ⅎ 𝑥 𝑦
24	22 15 23	nfbr	⊢ Ⅎ 𝑥 seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦
25	6 20 24	nf3an	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 )
26	4 25	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 )
27		nfcv	⊢ Ⅎ 𝑥 ℕ
28		nfcv	⊢ Ⅎ 𝑥 𝑓
29		nfcv	⊢ Ⅎ 𝑥 ( 1 ... 𝑚 )
30	28 29 1	nff1o	⊢ Ⅎ 𝑥 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴
31		nfcv	⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑛 )
32	31 2	nfcsbw	⊢ Ⅎ 𝑥 ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵
33	27 32	nfmpt	⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
34	11 9 33	nfseq	⊢ Ⅎ 𝑥 seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) )
35	34 21	nffv	⊢ Ⅎ 𝑥 ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
36	35	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 )
37	30 36	nfan	⊢ Ⅎ 𝑥 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
38	37	nfex	⊢ Ⅎ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
39	27 38	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
40	26 39	nfor	⊢ Ⅎ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
41	40	nfiotaw	⊢ Ⅎ 𝑥 ( ℩ 𝑦 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑧 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑦 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
42	3 41	nfcxfr	⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝐴 𝐵