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

Theorem nfcprod 14858
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 14853 . 2 𝑘𝐴 𝐵 = (℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 nfcv 2947 . . . . 5 𝑥
3 nfcprod.1 . . . . . . 7 𝑥𝐴
4 nfcv 2947 . . . . . . 7 𝑥(ℤ𝑚)
53, 4nfss 3788 . . . . . 6 𝑥 𝐴 ⊆ (ℤ𝑚)
6 nfv 2008 . . . . . . . . 9 𝑥 𝑧 ≠ 0
7 nfcv 2947 . . . . . . . . . . 11 𝑥𝑛
8 nfcv 2947 . . . . . . . . . . 11 𝑥 ·
93nfcri 2941 . . . . . . . . . . . . 13 𝑥 𝑘𝐴
10 nfcprod.2 . . . . . . . . . . . . 13 𝑥𝐵
11 nfcv 2947 . . . . . . . . . . . . 13 𝑥1
129, 10, 11nfif 4305 . . . . . . . . . . . 12 𝑥if(𝑘𝐴, 𝐵, 1)
132, 12nfmpt 4936 . . . . . . . . . . 11 𝑥(𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
147, 8, 13nfseq 13030 . . . . . . . . . 10 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
15 nfcv 2947 . . . . . . . . . 10 𝑥
16 nfcv 2947 . . . . . . . . . 10 𝑥𝑧
1714, 15, 16nfbr 4887 . . . . . . . . 9 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧
186, 17nfan 1993 . . . . . . . 8 𝑥(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
1918nfex 2332 . . . . . . 7 𝑥𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
204, 19nfrex 3193 . . . . . 6 𝑥𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
21 nfcv 2947 . . . . . . . 8 𝑥𝑚
2221, 8, 13nfseq 13030 . . . . . . 7 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
23 nfcv 2947 . . . . . . 7 𝑥𝑦
2422, 15, 23nfbr 4887 . . . . . 6 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
255, 20, 24nf3an 1996 . . . . 5 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
262, 25nfrex 3193 . . . 4 𝑥𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
27 nfcv 2947 . . . . 5 𝑥
28 nfcv 2947 . . . . . . . 8 𝑥𝑓
29 nfcv 2947 . . . . . . . 8 𝑥(1...𝑚)
3028, 29, 3nff1o 6348 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
31 nfcv 2947 . . . . . . . . . . . 12 𝑥(𝑓𝑛)
3231, 10nfcsb 3743 . . . . . . . . . . 11 𝑥(𝑓𝑛) / 𝑘𝐵
3327, 32nfmpt 4936 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3411, 8, 33nfseq 13030 . . . . . . . . 9 𝑥seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3534, 21nffv 6415 . . . . . . . 8 𝑥(seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3635nfeq2 2963 . . . . . . 7 𝑥 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3730, 36nfan 1993 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3837nfex 2332 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3927, 38nfrex 3193 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4026, 39nfor 1999 . . 3 𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
4140nfiota 6065 . 2 𝑥(℩𝑦(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
421, 41nfcxfr 2945 1 𝑥𝑘𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2158  wnfc 2934  wne 2977  wrex 3096  csb 3725  wss 3766  ifcif 4276   class class class wbr 4840  cmpt 4919  cio 6059  1-1-ontowf1o 6097  cfv 6098  (class class class)co 6871  0cc0 10218  1c1 10219   · cmul 10223  cn 11302  cz 11639  cuz 11900  ...cfz 12545  seqcseq 13020  cli 14434  cprod 14852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-mpt 4920  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-seq 13021  df-prod 14853
This theorem is referenced by:  fprod2dlem  14927  fprodcom2  14931  fprodcn  40309  fprodcncf  40591
  Copyright terms: Public domain W3C validator