Theorem pwundifOLD

Description: Obsolete proof of pwundif as of 26-Dec-2023. (Contributed by NM, 25-Mar-2007) (Proof shortened by Thierry Arnoux, 20-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	pwundifOLD	$$⊢𝒫\left(A\cup B\right)=\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		undif1	$$⊢\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A=𝒫\left(A\cup B\right)\cup 𝒫A$$
2		pwunss	$$⊢𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$
3		unss	$$⊢\left(𝒫A\subseteq 𝒫\left(A\cup B\right)\wedge 𝒫B\subseteq 𝒫\left(A\cup B\right)\right)\leftrightarrow 𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$
4	2 3	mpbir	$$⊢\left(𝒫A\subseteq 𝒫\left(A\cup B\right)\wedge 𝒫B\subseteq 𝒫\left(A\cup B\right)\right)$$
5	4	simpli	$$⊢𝒫A\subseteq 𝒫\left(A\cup B\right)$$
6		ssequn2	$$⊢𝒫A\subseteq 𝒫\left(A\cup B\right)\leftrightarrow 𝒫\left(A\cup B\right)\cup 𝒫A=𝒫\left(A\cup B\right)$$
7	5 6	mpbi	$$⊢𝒫\left(A\cup B\right)\cup 𝒫A=𝒫\left(A\cup B\right)$$
8	1 7	eqtr2i	$$⊢𝒫\left(A\cup B\right)=\left(𝒫\left(A\cup B\right)\setminus 𝒫A\right)\cup 𝒫A$$