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

Theorem prodex 15322
 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 15321 . 2 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 iotaex 6320 . 2 (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∈ V
31, 2eqeltri 2848 1 𝑘𝐴 𝐵 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  Vcvv 3409  ⦋csb 3807   ⊆ wss 3860  ifcif 4423   class class class wbr 5036   ↦ cmpt 5116  ℩cio 6297  –1-1-onto→wf1o 6339  ‘cfv 6340  (class class class)co 7156  0cc0 10588  1c1 10589   · cmul 10593  ℕcn 11687  ℤcz 12033  ℤ≥cuz 12295  ...cfz 12952  seqcseq 13431   ⇝ cli 14902  ∏cprod 15320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-nul 5180 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-sn 4526  df-pr 4528  df-uni 4802  df-iota 6299  df-prod 15321 This theorem is referenced by:  risefacval  15423  fallfacval  15424  prmoval  16438  fprodsubrecnncnvlem  42960  fprodaddrecnncnvlem  42962  etransclem13  43300  ovnlecvr  43608  ovncvrrp  43614  hoidmvval  43627  vonioolem1  43730
 Copyright terms: Public domain W3C validator