Theorem pwssun

Description: The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of Mendelson p. 235. (Contributed by NM, 23-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		ssequn2	$$⊢B\subseteq A\leftrightarrow A\cup B=A$$
2		pweq	$$⊢A\cup B=A\to 𝒫\left(A\cup B\right)=𝒫A$$
3		eqimss	$$⊢𝒫\left(A\cup B\right)=𝒫A\to 𝒫\left(A\cup B\right)\subseteq 𝒫A$$
4	2 3	syl	$$⊢A\cup B=A\to 𝒫\left(A\cup B\right)\subseteq 𝒫A$$
5	1 4	sylbi	$$⊢B\subseteq A\to 𝒫\left(A\cup B\right)\subseteq 𝒫A$$
6		ssequn1	$$⊢A\subseteq B\leftrightarrow A\cup B=B$$
7		pweq	$$⊢A\cup B=B\to 𝒫\left(A\cup B\right)=𝒫B$$
8		eqimss	$$⊢𝒫\left(A\cup B\right)=𝒫B\to 𝒫\left(A\cup B\right)\subseteq 𝒫B$$
9	7 8	syl	$$⊢A\cup B=B\to 𝒫\left(A\cup B\right)\subseteq 𝒫B$$
10	6 9	sylbi	$$⊢A\subseteq B\to 𝒫\left(A\cup B\right)\subseteq 𝒫B$$
11	5 10	orim12i	$$⊢\left(B\subseteq A\vee A\subseteq B\right)\to \left(𝒫\left(A\cup B\right)\subseteq 𝒫A\vee 𝒫\left(A\cup B\right)\subseteq 𝒫B\right)$$
12	11	orcoms	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\to \left(𝒫\left(A\cup B\right)\subseteq 𝒫A\vee 𝒫\left(A\cup B\right)\subseteq 𝒫B\right)$$
13		ssun	$$⊢\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\vee 𝒫\left(A\cup B\right)\subseteq 𝒫B\right)\to 𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B$$
14	12 13	syl	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\to 𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B$$
15		vex	$$⊢x\in \mathrm{V}$$
16	15	snss	$$⊢x\in A\leftrightarrow \left\{x\right\}\subseteq A$$
17		vex	$$⊢y\in \mathrm{V}$$
18	17	snss	$$⊢y\in B\leftrightarrow \left\{y\right\}\subseteq B$$
19		unss12	$$⊢\left(\left\{x\right\}\subseteq A\wedge \left\{y\right\}\subseteq B\right)\to \left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B$$
20	16 18 19	syl2anb	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B$$
21		zfpair2	$$⊢\left\{x,y\right\}\in \mathrm{V}$$
22	21	elpw	$$⊢\left\{x,y\right\}\in 𝒫\left(A\cup B\right)\leftrightarrow \left\{x,y\right\}\subseteq A\cup B$$
23		df-pr	$$⊢\left\{x,y\right\}=\left\{x\right\}\cup \left\{y\right\}$$
24	23	sseq1i	$$⊢\left\{x,y\right\}\subseteq A\cup B\leftrightarrow \left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B$$
25	22 24	bitr2i	$$⊢\left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B\leftrightarrow \left\{x,y\right\}\in 𝒫\left(A\cup B\right)$$
26	20 25	sylib	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x,y\right\}\in 𝒫\left(A\cup B\right)$$
27		ssel	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(\left\{x,y\right\}\in 𝒫\left(A\cup B\right)\to \left\{x,y\right\}\in \left(𝒫A\cup 𝒫B\right)\right)$$
28	26 27	syl5	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(\left(x\in A\wedge y\in B\right)\to \left\{x,y\right\}\in \left(𝒫A\cup 𝒫B\right)\right)$$
29	28	expcomd	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(y\in B\to \left(x\in A\to \left\{x,y\right\}\in \left(𝒫A\cup 𝒫B\right)\right)\right)$$
30	29	imp31	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge x\in A\right)\to \left\{x,y\right\}\in \left(𝒫A\cup 𝒫B\right)$$
31		elun	$$⊢\left\{x,y\right\}\in \left(𝒫A\cup 𝒫B\right)\leftrightarrow \left(\left\{x,y\right\}\in 𝒫A\vee \left\{x,y\right\}\in 𝒫B\right)$$
32	30 31	sylib	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge x\in A\right)\to \left(\left\{x,y\right\}\in 𝒫A\vee \left\{x,y\right\}\in 𝒫B\right)$$
33	21	elpw	$$⊢\left\{x,y\right\}\in 𝒫A\leftrightarrow \left\{x,y\right\}\subseteq A$$
34	15 17	prss	$$⊢\left(x\in A\wedge y\in A\right)\leftrightarrow \left\{x,y\right\}\subseteq A$$
35	33 34	bitr4i	$$⊢\left\{x,y\right\}\in 𝒫A\leftrightarrow \left(x\in A\wedge y\in A\right)$$
36	35	simprbi	$$⊢\left\{x,y\right\}\in 𝒫A\to y\in A$$
37	21	elpw	$$⊢\left\{x,y\right\}\in 𝒫B\leftrightarrow \left\{x,y\right\}\subseteq B$$
38	15 17	prss	$$⊢\left(x\in B\wedge y\in B\right)\leftrightarrow \left\{x,y\right\}\subseteq B$$
39	37 38	bitr4i	$$⊢\left\{x,y\right\}\in 𝒫B\leftrightarrow \left(x\in B\wedge y\in B\right)$$
40	39	simplbi	$$⊢\left\{x,y\right\}\in 𝒫B\to x\in B$$
41	36 40	orim12i	$$⊢\left(\left\{x,y\right\}\in 𝒫A\vee \left\{x,y\right\}\in 𝒫B\right)\to \left(y\in A\vee x\in B\right)$$
42	32 41	syl	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge x\in A\right)\to \left(y\in A\vee x\in B\right)$$
43	42	ord	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge x\in A\right)\to \left(\neg y\in A\to x\in B\right)$$
44	43	impancom	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge \neg y\in A\right)\to \left(x\in A\to x\in B\right)$$
45	44	ssrdv	$$⊢\left(\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge y\in B\right)\wedge \neg y\in A\right)\to A\subseteq B$$
46	45	exp31	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(y\in B\to \left(\neg y\in A\to A\subseteq B\right)\right)$$
47		con1b	$$⊢\left(\neg y\in A\to A\subseteq B\right)\leftrightarrow \left(\neg A\subseteq B\to y\in A\right)$$
48	46 47	imbitrdi	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(y\in B\to \left(\neg A\subseteq B\to y\in A\right)\right)$$
49	48	com23	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(\neg A\subseteq B\to \left(y\in B\to y\in A\right)\right)$$
50	49	imp	$$⊢\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge \neg A\subseteq B\right)\to \left(y\in B\to y\in A\right)$$
51	50	ssrdv	$$⊢\left(𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\wedge \neg A\subseteq B\right)\to B\subseteq A$$
52	51	ex	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(\neg A\subseteq B\to B\subseteq A\right)$$
53	52	orrd	$$⊢𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B\to \left(A\subseteq B\vee B\subseteq A\right)$$
54	14 53	impbii	$$⊢\left(A\subseteq B\vee B\subseteq A\right)\leftrightarrow 𝒫\left(A\cup B\right)\subseteq 𝒫A\cup 𝒫B$$