Theorem dmplp

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

	Ref	Expression
Assertion	dmplp	⊢ dom +P = ( P × P )

Proof

Step	Hyp	Ref	Expression
1		df-plp	⊢ +P = ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑧 ∣ ∃ 𝑢 ∈ 𝑥 ∃ 𝑣 ∈ 𝑦 𝑧 = ( 𝑢 +Q 𝑣 ) } )
2		addclnq	⊢ ( ( 𝑢 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑢 +Q 𝑣 ) ∈ Q )
3	1 2	genpdm	⊢ dom +P = ( P × P )