Theorem pwun

Description: The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of Enderton p. 28. (Contributed by NM, 23-Nov-2003)

	Ref	Expression
Assertion	pwun	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow 𝒫\left(A\cup B\right)=𝒫A\cup 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		pwunss	$$⊢𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)$$
2	1	biantru	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\leftrightarrow \left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge 𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)\right)$$
3		pwssun	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow 𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B$$
4		eqss	$$⊢𝒫\left(A\cup B\right)=𝒫A\cup 𝒫B\leftrightarrow \left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge 𝒫A\cup 𝒫B\subseteq 𝒫\left(A\cup B\right)\right)$$
5	2 3 4	3bitr4i	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow 𝒫\left(A\cup B\right)=𝒫A\cup 𝒫B$$