Definition df-mp

Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mp	|- .P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmp	|- .P.
1		vx	|- x
2		cnp	|- P.
3		vy	|- y
4		vw	|- w
5		vv	|- v
6	1	cv	|- x
7		vu	|- u
8	3	cv	|- y
9	4	cv	|- w
10	5	cv	|- v
11		cmq	|- .Q
12	7	cv	|- u
13	10 12 11	co	|- ( v .Q u )
14	9 13	wceq	|- w = ( v .Q u )
15	14 7 8	wrex	|- E. u e. y w = ( v .Q u )
16	15 5 6	wrex	|- E. v e. x E. u e. y w = ( v .Q u )
17	16 4	cab	|- { w | E. v e. x E. u e. y w = ( v .Q u ) }
18	1 3 2 2 17	cmpo	|- ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )
19	0 18	wceq	|- .P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )