Metamath Proof Explorer

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 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 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 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑧 ( 𝑧 ≠ 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 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 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 ⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝐴 𝐵