Theorem pwunssOLD

Description: Obsolete version of pwunss as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ssun	$$⊢\left(x\subseteq A\vee x\subseteq B\right)\to x\subseteq A\cup B$$
2		elun	$$⊢x\in \left(𝒫A\cup 𝒫B\right)\leftrightarrow \left(x\in 𝒫A\vee x\in 𝒫B\right)$$
3		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
4		velpw	$$⊢x\in 𝒫B\leftrightarrow x\subseteq B$$
5	3 4	orbi12i	$$⊢\left(x\in 𝒫A\vee x\in 𝒫B\right)\leftrightarrow \left(x\subseteq A\vee x\subseteq B\right)$$
6	2 5	bitri	$$⊢x\in \left(𝒫A\cup 𝒫B\right)\leftrightarrow \left(x\subseteq A\vee x\subseteq B\right)$$
7		velpw	$$⊢x\in 𝒫\left(A\cup B\right)\leftrightarrow x\subseteq A\cup B$$
8	1 6 7	3imtr4i	$$⊢x\in \left(𝒫A\cup 𝒫B\right)\to x\in 𝒫\left(A\cup B\right)$$
9	8	ssriv	$$⊢𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$