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	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mpomulf	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right):ℂ\times ℂ⟶ℂ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3	2 2	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
4		fex2	$$⊢\left(\left(x\in ℂ,y\in ℂ⟼xy\right):ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \left(x\in ℂ,y\in ℂ⟼xy\right)\in \mathrm{V}$$
5	1 3 2 4	mp3an	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)\in \mathrm{V}$$