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

Theorem nfcprod1 14857
Description: Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypothesis
Ref Expression
nfcprod1.1 𝑘𝐴
Assertion
Ref Expression
nfcprod1 𝑘𝑘𝐴 𝐵
Distinct variable group:   𝐴,𝑘
Allowed substitution hint:   𝐵(𝑘)

Proof of Theorem nfcprod1
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 2948 . . . . 5 𝑘
3 nfcprod1.1 . . . . . . 7 𝑘𝐴
4 nfcv 2948 . . . . . . 7 𝑘(ℤ𝑚)
53, 4nfss 3791 . . . . . 6 𝑘 𝐴 ⊆ (ℤ𝑚)
6 nfv 2005 . . . . . . . . 9 𝑘 𝑦 ≠ 0
7 nfcv 2948 . . . . . . . . . . 11 𝑘𝑛
8 nfcv 2948 . . . . . . . . . . 11 𝑘 ·
9 nfmpt1 4941 . . . . . . . . . . 11 𝑘(𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
107, 8, 9nfseq 13030 . . . . . . . . . 10 𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
11 nfcv 2948 . . . . . . . . . 10 𝑘
12 nfcv 2948 . . . . . . . . . 10 𝑘𝑦
1310, 11, 12nfbr 4891 . . . . . . . . 9 𝑘seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
146, 13nfan 1990 . . . . . . . 8 𝑘(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
1514nfex 2330 . . . . . . 7 𝑘𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
164, 15nfrex 3194 . . . . . 6 𝑘𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
17 nfcv 2948 . . . . . . . 8 𝑘𝑚
1817, 8, 9nfseq 13030 . . . . . . 7 𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
19 nfcv 2948 . . . . . . 7 𝑘𝑥
2018, 11, 19nfbr 4891 . . . . . 6 𝑘seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥
215, 16, 20nf3an 1993 . . . . 5 𝑘(𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
222, 21nfrex 3194 . . . 4 𝑘𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
23 nfcv 2948 . . . . 5 𝑘
24 nfcv 2948 . . . . . . . 8 𝑘𝑓
25 nfcv 2948 . . . . . . . 8 𝑘(1...𝑚)
2624, 25, 3nff1o 6347 . . . . . . 7 𝑘 𝑓:(1...𝑚)–1-1-onto𝐴
27 nfcv 2948 . . . . . . . . . 10 𝑘1
28 nfcsb1v 3744 . . . . . . . . . . 11 𝑘(𝑓𝑛) / 𝑘𝐵
2923, 28nfmpt 4940 . . . . . . . . . 10 𝑘(𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
3027, 8, 29nfseq 13030 . . . . . . . . 9 𝑘seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
3130, 17nffv 6414 . . . . . . . 8 𝑘(seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3231nfeq2 2964 . . . . . . 7 𝑘 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
3326, 32nfan 1990 . . . . . 6 𝑘(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3433nfex 2330 . . . . 5 𝑘𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3523, 34nfrex 3194 . . . 4 𝑘𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
3622, 35nfor 1996 . . 3 𝑘(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
3736nfiota 6064 . 2 𝑘(℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
381, 37nfcxfr 2946 1 𝑘𝑘𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2156  wnfc 2935  wne 2978  wrex 3097  csb 3728  wss 3769  ifcif 4279   class class class wbr 4844  cmpt 4923  cio 6058  1-1-ontowf1o 6096  cfv 6097  (class class class)co 6870  0cc0 10217  1c1 10218   · cmul 10222  cn 11301  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 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  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 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-seq 13021  df-prod 14853
This theorem is referenced by:  fprodcn  40306  dvmptfprod  40634  vonicc  41375
  Copyright terms: Public domain W3C validator