Theorem plpv

Description: Value of addition on positive reals. (Contributed by NM, 28-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	plpv	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{+}_{𝑷}B=\left\{x|\exists y\in A\exists z\in Bx=y{+}_{𝑸}z\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-plp	$$⊢{+}_{𝑷}=\left(u\in 𝑷,v\in 𝑷⟼\left\{f|\exists g\in u\exists h\in vf=g{+}_{𝑸}h\right\}\right)$$
2		addclnq	$$⊢\left(g\in 𝑸\wedge h\in 𝑸\right)\to g{+}_{𝑸}h\in 𝑸$$
3	1 2	genpv	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{+}_{𝑷}B=\left\{x|\exists y\in A\exists z\in Bx=y{+}_{𝑸}z\right\}$$