Metamath Proof Explorer


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 )