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

Theorem nfcprod 15946
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 15941 . 2 𝑘𝐴 𝐵 = (℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2904 . . . . 5 𝑥
3 nfcprod.1 . . . . . . 7 𝑥𝐴
4 nfcv 2904 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3975 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfv 1913 . . . . . . . . 9 𝑥 𝑧 ≠ 0
7 nfcv 2904 . . . . . . . . . . 11 𝑥𝑛
8 nfcv 2904 . . . . . . . . . . 11 𝑥 ·
93nfcri 2896 . . . . . . . . . . . . 13 𝑥 𝑘𝐴
10 nfcprod.2 . . . . . . . . . . . . 13 𝑥𝐵
11 nfcv 2904 . . . . . . . . . . . . 13 𝑥1
129, 10, 11nfif 4555 . . . . . . . . . . . 12 𝑥if(𝑘𝐴, 𝐵, 1)
132, 12nfmpt 5248 . . . . . . . . . . 11 𝑥(𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
147, 8, 13nfseq 14053 . . . . . . . . . 10 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
15 nfcv 2904 . . . . . . . . . 10 𝑥
16 nfcv 2904 . . . . . . . . . 10 𝑥𝑧
1714, 15, 16nfbr 5189 . . . . . . . . 9 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧
186, 17nfan 1898 . . . . . . . 8 𝑥(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
1918nfex 2323 . . . . . . 7 𝑥𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
204, 19nfrexw 3312 . . . . . 6 𝑥𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
21 nfcv 2904 . . . . . . . 8 𝑥𝑚
2221, 8, 13nfseq 14053 . . . . . . 7 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
23 nfcv 2904 . . . . . . 7 𝑥𝑦
2422, 15, 23nfbr 5189 . . . . . 6 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
255, 20, 24nf3an 1900 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
262, 25nfrexw 3312 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
27 nfcv 2904 . . . . 5 𝑥
28 nfcv 2904 . . . . . . . 8 𝑥𝑓
29 nfcv 2904 . . . . . . . 8 𝑥(1...𝑚)
3028, 29, 3nff1o 6845 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
31 nfcv 2904 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
3231, 10nfcsbw 3924 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
3327, 32nfmpt 5248 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3411, 8, 33nfseq 14053 . . . . . . . . 9 𝑥seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3534, 21nffv 6915 . . . . . . . 8 𝑥(seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3635nfeq2 2922 . . . . . . 7 𝑥 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3730, 36nfan 1898 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3837nfex 2323 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3927, 38nfrexw 3312 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4026, 39nfor 1903 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4140nfiotaw 6517 . 2 𝑥(℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
421, 41nfcxfr 2902 1 𝑥𝑘𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 395  wo 847  w3a 1086   = wceq 1539  wex 1778  wcel 2107  wnfc 2889  wne 2939  wrex 3069  csb 3898  wss 3950  ifcif 4524   class class class wbr 5142  cmpt 5224  cio 6511  1-1-ontowf1o 6559  cfv 6560  (class class class)co 7432  0cc0 11156  1c1 11157   · cmul 11161  cn 12267  cz 12615  cuz 12879  ...cfz 13548  seqcseq 14043  cli 15521  cprod 15940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-seq 14044  df-prod 15941
This theorem is referenced by:  fprod2dlem  16017  fprodcom2  16021  fprodcn  45620  fprodcncf  45920
  Copyright terms: Public domain W3C validator