Metamath Proof Explorer

Theorem prodex

Description: A product is a set. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodex ⊢ ∏ k ∈ A B ∈ V

Proof

Step Hyp Ref Expression
1 df-prod ⊢ ∏ k ∈ A B = ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
2 iotaex ⊢ ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m ∈ V
3 1 2 eqeltri ⊢ ∏ k ∈ A B ∈ V