Theorem dmplp

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

	Ref	Expression
Assertion	dmplp	$$⊢\mathrm{dom}{+}_{𝑷}=𝑷\times 𝑷$$

Proof

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