MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcprod Structured version   Visualization version   GIF version

Theorem nfcprod 15725
Description: Bound-variable hypothesis builder for product: if 𝑥 is (effectively) not free in 𝐴 and 𝐵, it is not free in 𝑘𝐴𝐵. (Contributed by Scott Fenton, 1-Dec-2017.)
Hypotheses
Ref Expression
nfcprod.1 𝑥𝐴
nfcprod.2 𝑥𝐵
Assertion
Ref Expression
nfcprod 𝑥𝑘𝐴 𝐵
Distinct variable group:   𝑥,𝑘
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥,𝑘)

Proof of Theorem nfcprod
Dummy variables 𝑓 𝑚 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-prod 15720 . 2 𝑘𝐴 𝐵 = (℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2905 . . . . 5 𝑥
3 nfcprod.1 . . . . . . 7 𝑥𝐴
4 nfcv 2905 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3931 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfv 1917 . . . . . . . . 9 𝑥 𝑧 ≠ 0
7 nfcv 2905 . . . . . . . . . . 11 𝑥𝑛
8 nfcv 2905 . . . . . . . . . . 11 𝑥 ·
93nfcri 2892 . . . . . . . . . . . . 13 𝑥 𝑘𝐴
10 nfcprod.2 . . . . . . . . . . . . 13 𝑥𝐵
11 nfcv 2905 . . . . . . . . . . . . 13 𝑥1
129, 10, 11nfif 4511 . . . . . . . . . . . 12 𝑥if(𝑘𝐴, 𝐵, 1)
132, 12nfmpt 5207 . . . . . . . . . . 11 𝑥(𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
147, 8, 13nfseq 13841 . . . . . . . . . 10 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
15 nfcv 2905 . . . . . . . . . 10 𝑥
16 nfcv 2905 . . . . . . . . . 10 𝑥𝑧
1714, 15, 16nfbr 5147 . . . . . . . . 9 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧
186, 17nfan 1902 . . . . . . . 8 𝑥(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
1918nfex 2318 . . . . . . 7 𝑥𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
204, 19nfrexw 3294 . . . . . 6 𝑥𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
21 nfcv 2905 . . . . . . . 8 𝑥𝑚
2221, 8, 13nfseq 13841 . . . . . . 7 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
23 nfcv 2905 . . . . . . 7 𝑥𝑦
2422, 15, 23nfbr 5147 . . . . . 6 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
255, 20, 24nf3an 1904 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
262, 25nfrexw 3294 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
27 nfcv 2905 . . . . 5 𝑥
28 nfcv 2905 . . . . . . . 8 𝑥𝑓
29 nfcv 2905 . . . . . . . 8 𝑥(1...𝑚)
3028, 29, 3nff1o 6774 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
31 nfcv 2905 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
3231, 10nfcsbw 3877 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
3327, 32nfmpt 5207 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3411, 8, 33nfseq 13841 . . . . . . . . 9 𝑥seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3534, 21nffv 6844 . . . . . . . 8 𝑥(seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3635nfeq2 2922 . . . . . . 7 𝑥 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3730, 36nfan 1902 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3837nfex 2318 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3927, 38nfrexw 3294 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4026, 39nfor 1907 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4140nfiotaw 6444 . 2 𝑥(℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
421, 41nfcxfr 2903 1 𝑥𝑘𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 397  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wnfc 2885  wne 2941  wrex 3071  csb 3850  wss 3905  ifcif 4481   class class class wbr 5100  cmpt 5183  cio 6438  1-1-ontowf1o 6487  cfv 6488  (class class class)co 7346  0cc0 10981  1c1 10982   · cmul 10986  cn 12083  cz 12429  cuz 12692  ...cfz 13349  seqcseq 13831  cli 15297  cprod 15719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-opab 5163  df-mpt 5184  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7349  df-oprab 7350  df-mpo 7351  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-seq 13832  df-prod 15720
This theorem is referenced by:  fprod2dlem  15794  fprodcom2  15798  fprodcn  43529  fprodcncf  43829
  Copyright terms: Public domain W3C validator