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	|- ( x e. CC , y e. CC |-> ( x x. y ) ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mpomulf	|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
2		cnex	|- CC e. _V
3	2 2	xpex	|- ( CC X. CC ) e. _V
4		fex2	|- ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V /\ CC e. _V ) -> ( x e. CC , y e. CC |-> ( x x. y ) ) e. _V )
5	1 3 2 4	mp3an	|- ( x e. CC , y e. CC |-> ( x x. y ) ) e. _V