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	$$⊢{\cdot }_{𝑷}=\left(x\in 𝑷,y\in 𝑷⟼\left\{w|\exists v\in x\exists u\in yw=v{\cdot }_{𝑸}u\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmp	$$class{\cdot }_{𝑷}$$
1		vx	$$setvarx$$
2		cnp	$$class𝑷$$
3		vy	$$setvary$$
4		vw	$$setvarw$$
5		vv	$$setvarv$$
6	1	cv	$$setvarx$$
7		vu	$$setvaru$$
8	3	cv	$$setvary$$
9	4	cv	$$setvarw$$
10	5	cv	$$setvarv$$
11		cmq	$$class{\cdot }_{𝑸}$$
12	7	cv	$$setvaru$$
13	10 12 11	co	$$class\left(v{\cdot }_{𝑸}u\right)$$
14	9 13	wceq	$$wffw=v{\cdot }_{𝑸}u$$
15	14 7 8	wrex	$$wff\exists u\in yw=v{\cdot }_{𝑸}u$$
16	15 5 6	wrex	$$wff\exists v\in x\exists u\in yw=v{\cdot }_{𝑸}u$$
17	16 4	cab	$$class\left\{w|\exists v\in x\exists u\in yw=v{\cdot }_{𝑸}u\right\}$$
18	1 3 2 2 17	cmpo	$$class\left(x\in 𝑷,y\in 𝑷⟼\left\{w|\exists v\in x\exists u\in yw=v{\cdot }_{𝑸}u\right\}\right)$$
19	0 18	wceq	$$wff{\cdot }_{𝑷}=\left(x\in 𝑷,y\in 𝑷⟼\left\{w|\exists v\in x\exists u\in yw=v{\cdot }_{𝑸}u\right\}\right)$$