Theorem mpomulex

Description: The multiplication operation is a set. Version of mulex using maps-to notation , which does not require ax-mulf . (Contributed by GG, 16-Mar-2025)

	Ref	Expression
Assertion	mpomulex	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		mpomulf	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ
2		cnex	⊢ ℂ ∈ V
3	2 2	xpex	⊢ ( ℂ × ℂ ) ∈ V
4		fex2	⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ∧ ℂ ∈ V ) → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ V )
5	1 3 2 4	mp3an	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ V