Theorem mpomulf

Description: Multiplication is an operation on complex numbers. Version of ax-mulf using maps-to notation, proved from the axioms of set theory and ax-mulcl . (Contributed by GG, 16-Mar-2025)

	Ref	Expression
Assertion	mpomulf	|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( x e. CC , y e. CC |-> ( x x. y ) )
2		ovex	|- ( x x. y ) e. _V
3	1 2	fnmpoi	|- ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC )
4		simpll	|- ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> x e. CC )
5		simplr	|- ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> y e. CC )
6		mulcl	|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
7		eleq1a	|- ( ( x x. y ) e. CC -> ( z = ( x x. y ) -> z e. CC ) )
8	6 7	syl	|- ( ( x e. CC /\ y e. CC ) -> ( z = ( x x. y ) -> z e. CC ) )
9	8	imp	|- ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> z e. CC )
10	4 5 9	3jca	|- ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> ( x e. CC /\ y e. CC /\ z e. CC ) )
11	10	ssoprab2i	|- { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) } C_ { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
12		df-mpo	|- ( x e. CC , y e. CC |-> ( x x. y ) ) = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) }
13		dfxp3	|- ( ( CC X. CC ) X. CC ) = { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
14	11 12 13	3sstr4i	|- ( x e. CC , y e. CC |-> ( x x. y ) ) C_ ( ( CC X. CC ) X. CC )
15		dff2	|- ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( x e. CC , y e. CC |-> ( x x. y ) ) C_ ( ( CC X. CC ) X. CC ) ) )
16	3 14 15	mpbir2an	|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC