Theorem pwunss

Description: The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003) Remove use of ax-sep , ax-nul , ax-pr and shorten proof. (Revised by BJ, 13-Apr-2024)

	Ref	Expression
Assertion	pwunss	$$⊢𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup B$$
2	1	sspwi	$$⊢𝒫A\subseteq 𝒫\left(A\cup B\right)$$
3		ssun2	$$⊢B\subseteq A\cup B$$
4	3	sspwi	$$⊢𝒫B\subseteq 𝒫\left(A\cup B\right)$$
5	2 4	unssi	$$⊢𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$