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