Theorem prodex 15807

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.

Step	Hyp	Ref	Expression
1		df-prod 15806	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		iotaex 6452	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) ∈ V
3	1, 2	eqeltri 2827	1 ⊢ ∏𝑘 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ≠ wne 2928  ∃wrex 3056  Vcvv 3436  ⦋csb 3845   ⊆ wss 3897  ifcif 4470   class class class wbr 5086   ↦ cmpt 5167  ℩cio 6430  –1-1-onto→wf1o 6475  ‘cfv 6476  (class class class)co 7341  0cc0 11001  1c1 11002   · cmul 11006  ℕcn 12120  ℤcz 12463  ℤ_≥cuz 12727  ...cfz 13402  seqcseq 13903   ⇝ cli 15386  ∏cprod 15805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-sn 4572  df-pr 4574  df-uni 4855  df-iota 6432  df-prod 15806

This theorem is referenced by:  risefacval  15910  fallfacval  15911  prmoval  16940  fprodsubrecnncnvlem  45945  fprodaddrecnncnvlem  45947  etransclem13  46285  ovnlecvr  46596  ovncvrrp  46602  hoidmvval  46615  vonioolem1  46718