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

Theorem prodex 14843
 Description: A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.)
Assertion
Ref Expression
prodex 𝑘𝐴 𝐵 ∈ V

Proof of Theorem prodex
Dummy variables 𝑓 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-prod 14842 . 2 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 6011 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2845 1 𝑘𝐴 𝐵 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 382   ∨ wo 826   ∧ w3a 1070   = wceq 1630  ∃wex 1851   ∈ wcel 2144   ≠ wne 2942  ∃wrex 3061  Vcvv 3349  ⦋csb 3680   ⊆ wss 3721  ifcif 4223   class class class wbr 4784   ↦ cmpt 4861  ℩cio 5992  –1-1-onto→wf1o 6030  ‘cfv 6031  (class class class)co 6792  0cc0 10137  1c1 10138   · cmul 10142  ℕcn 11221  ℤcz 11578  ℤ≥cuz 11887  ...cfz 12532  seqcseq 13007   ⇝ cli 14422  ∏cprod 14841 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-nul 4920 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-sn 4315  df-pr 4317  df-uni 4573  df-iota 5994  df-prod 14842 This theorem is referenced by:  risefacval  14944  fallfacval  14945  prmoval  15943  fprodsubrecnncnvlem  40633  fprodaddrecnncnvlem  40635  etransclem13  40975  ovnlecvr  41286  ovncvrrp  41292  hoidmvval  41305  vonioolem1  41408
 Copyright terms: Public domain W3C validator