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