Theorem dmmp

Description: Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	dmmp	$$⊢\mathrm{dom}{\cdot }_{𝑷}=𝑷\times 𝑷$$

Proof

Step	Hyp	Ref	Expression
1		df-mp	$$⊢{\cdot }_{𝑷}=\left(x\in 𝑷,y\in 𝑷⟼\left\{z|\exists u\in x\exists v\in yz=u{\cdot }_{𝑸}v\right\}\right)$$
2		mulclnq	$$⊢\left(u\in 𝑸\wedge v\in 𝑸\right)\to u{\cdot }_{𝑸}v\in 𝑸$$
3	1 2	genpdm	$$⊢\mathrm{dom}{\cdot }_{𝑷}=𝑷\times 𝑷$$