ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcprod GIF version

Theorem nfcprod 11547
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-proddc 11543 . 2 𝑘𝐴 𝐵 = (℩𝑦(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
2 nfcv 2319 . . . . 5 𝑥
3 nfcprod.1 . . . . . . . 8 𝑥𝐴
4 nfcv 2319 . . . . . . . 8 𝑥(ℤ𝑚)
53, 4nfss 3148 . . . . . . 7 𝑥 𝐴 ⊆ (ℤ𝑚)
63nfcri 2313 . . . . . . . . 9 𝑥 𝑗𝐴
76nfdc 1659 . . . . . . . 8 𝑥DECID 𝑗𝐴
84, 7nfralxy 2515 . . . . . . 7 𝑥𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴
95, 8nfan 1565 . . . . . 6 𝑥(𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
10 nfv 1528 . . . . . . . . . 10 𝑥 𝑧 # 0
11 nfcv 2319 . . . . . . . . . . . 12 𝑥𝑛
12 nfcv 2319 . . . . . . . . . . . 12 𝑥 ·
133nfcri 2313 . . . . . . . . . . . . . 14 𝑥 𝑘𝐴
14 nfcprod.2 . . . . . . . . . . . . . 14 𝑥𝐵
15 nfcv 2319 . . . . . . . . . . . . . 14 𝑥1
1613, 14, 15nfif 3562 . . . . . . . . . . . . 13 𝑥if(𝑘𝐴, 𝐵, 1)
172, 16nfmpt 4092 . . . . . . . . . . . 12 𝑥(𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
1811, 12, 17nfseq 10441 . . . . . . . . . . 11 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
19 nfcv 2319 . . . . . . . . . . 11 𝑥
20 nfcv 2319 . . . . . . . . . . 11 𝑥𝑧
2118, 19, 20nfbr 4046 . . . . . . . . . 10 𝑥seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧
2210, 21nfan 1565 . . . . . . . . 9 𝑥(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
2322nfex 1637 . . . . . . . 8 𝑥𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
244, 23nfrexxy 2516 . . . . . . 7 𝑥𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧)
25 nfcv 2319 . . . . . . . . 9 𝑥𝑚
2625, 12, 17nfseq 10441 . . . . . . . 8 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
27 nfcv 2319 . . . . . . . 8 𝑥𝑦
2826, 19, 27nfbr 4046 . . . . . . 7 𝑥seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
2924, 28nfan 1565 . . . . . 6 𝑥(∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
309, 29nfan 1565 . . . . 5 𝑥((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
312, 30nfrexxy 2516 . . . 4 𝑥𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦))
32 nfcv 2319 . . . . 5 𝑥
33 nfcv 2319 . . . . . . . 8 𝑥𝑓
34 nfcv 2319 . . . . . . . 8 𝑥(1...𝑚)
3533, 34, 3nff1o 5455 . . . . . . 7 𝑥 𝑓:(1...𝑚)–1-1-onto𝐴
36 nfv 1528 . . . . . . . . . . . 12 𝑥 𝑛𝑚
37 nfcv 2319 . . . . . . . . . . . . 13 𝑥(𝑓𝑛)
3837, 14nfcsb 3094 . . . . . . . . . . . 12 𝑥(𝑓𝑛) / 𝑘𝐵
3936, 38, 15nfif 3562 . . . . . . . . . . 11 𝑥if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)
4032, 39nfmpt 4092 . . . . . . . . . 10 𝑥(𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))
4115, 12, 40nfseq 10441 . . . . . . . . 9 𝑥seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))
4241, 25nffv 5521 . . . . . . . 8 𝑥(seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)
4342nfeq2 2331 . . . . . . 7 𝑥 𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)
4435, 43nfan 1565 . . . . . 6 𝑥(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
4544nfex 1637 . . . . 5 𝑥𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
4632, 45nfrexxy 2516 . . . 4 𝑥𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
4731, 46nfor 1574 . . 3 𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))
4847nfiotaw 5178 . 2 𝑥(℩𝑦(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑧(𝑧 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑧) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
491, 48nfcxfr 2316 1 𝑥𝑘𝐴 𝐵
Colors of variables: wff set class
Syntax hints:  wa 104  wo 708  DECID wdc 834   = wceq 1353  wex 1492  wcel 2148  wnfc 2306  wral 2455  wrex 2456  csb 3057  wss 3129  ifcif 3534   class class class wbr 4000  cmpt 4061  cio 5172  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  0cc0 7802  1c1 7803   · cmul 7807  cle 7983   # cap 8528  cn 8908  cz 9242  cuz 9517  ...cfz 9995  seqcseq 10431  cli 11270  cprod 11542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-mpt 4063  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-recs 6300  df-frec 6386  df-seqfrec 10432  df-proddc 11543
This theorem is referenced by:  fprod2dlemstep  11614  fprodcom2fi  11618
  Copyright terms: Public domain W3C validator