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. X. P. )

Proof

Step Hyp Ref Expression
1 df-plp 
 |-  +P. = ( x e. P. , y e. P. |-> { z | E. u e. x E. v e. y z = ( u +Q v ) } )
2 addclnq 
 |-  ( ( u e. Q. /\ v e. Q. ) -> ( u +Q v ) e. Q. )
3 1 2 genpdm 
 |-  dom +P. = ( P. X. P. )