Theorem pwpw0

Description: Compute the power set of the power set of the empty set. (See pw0 for the power set of the empty set.) Theorem 90 of Suppes p. 48. Although this theorem is a special case of pwsn , we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994)

	Ref	Expression
Assertion	pwpw0	$$⊢𝒫\left\{\varnothing \right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢x\subseteq \left\{\varnothing \right\}\leftrightarrow \forall y\left(y\in x\to y\in \left\{\varnothing \right\}\right)$$
2		velsn	$$⊢y\in \left\{\varnothing \right\}\leftrightarrow y=\varnothing$$
3	2	imbi2i	$$⊢\left(y\in x\to y\in \left\{\varnothing \right\}\right)\leftrightarrow \left(y\in x\to y=\varnothing \right)$$
4	3	albii	$$⊢\forall y\left(y\in x\to y\in \left\{\varnothing \right\}\right)\leftrightarrow \forall y\left(y\in x\to y=\varnothing \right)$$
5	1 4	bitri	$$⊢x\subseteq \left\{\varnothing \right\}\leftrightarrow \forall y\left(y\in x\to y=\varnothing \right)$$
6		neq0	$$⊢\neg x=\varnothing \leftrightarrow \exists yy\in x$$
7		exintr	$$⊢\forall y\left(y\in x\to y=\varnothing \right)\to \left(\exists yy\in x\to \exists y\left(y\in x\wedge y=\varnothing \right)\right)$$
8	6 7	biimtrid	$$⊢\forall y\left(y\in x\to y=\varnothing \right)\to \left(\neg x=\varnothing \to \exists y\left(y\in x\wedge y=\varnothing \right)\right)$$
9		exancom	$$⊢\exists y\left(y\in x\wedge y=\varnothing \right)\leftrightarrow \exists y\left(y=\varnothing \wedge y\in x\right)$$
10		dfclel	$$⊢\varnothing \in x\leftrightarrow \exists y\left(y=\varnothing \wedge y\in x\right)$$
11	9 10	bitr4i	$$⊢\exists y\left(y\in x\wedge y=\varnothing \right)\leftrightarrow \varnothing \in x$$
12		snssi	$$⊢\varnothing \in x\to \left\{\varnothing \right\}\subseteq x$$
13	11 12	sylbi	$$⊢\exists y\left(y\in x\wedge y=\varnothing \right)\to \left\{\varnothing \right\}\subseteq x$$
14	8 13	syl6	$$⊢\forall y\left(y\in x\to y=\varnothing \right)\to \left(\neg x=\varnothing \to \left\{\varnothing \right\}\subseteq x\right)$$
15	5 14	sylbi	$$⊢x\subseteq \left\{\varnothing \right\}\to \left(\neg x=\varnothing \to \left\{\varnothing \right\}\subseteq x\right)$$
16	15	anc2li	$$⊢x\subseteq \left\{\varnothing \right\}\to \left(\neg x=\varnothing \to \left(x\subseteq \left\{\varnothing \right\}\wedge \left\{\varnothing \right\}\subseteq x\right)\right)$$
17		eqss	$$⊢x=\left\{\varnothing \right\}\leftrightarrow \left(x\subseteq \left\{\varnothing \right\}\wedge \left\{\varnothing \right\}\subseteq x\right)$$
18	16 17	imbitrrdi	$$⊢x\subseteq \left\{\varnothing \right\}\to \left(\neg x=\varnothing \to x=\left\{\varnothing \right\}\right)$$
19	18	orrd	$$⊢x\subseteq \left\{\varnothing \right\}\to \left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)$$
20		0ss	$$⊢\varnothing \subseteq \left\{\varnothing \right\}$$
21		sseq1	$$⊢x=\varnothing \to \left(x\subseteq \left\{\varnothing \right\}\leftrightarrow \varnothing \subseteq \left\{\varnothing \right\}\right)$$
22	20 21	mpbiri	$$⊢x=\varnothing \to x\subseteq \left\{\varnothing \right\}$$
23		eqimss	$$⊢x=\left\{\varnothing \right\}\to x\subseteq \left\{\varnothing \right\}$$
24	22 23	jaoi	$$⊢\left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)\to x\subseteq \left\{\varnothing \right\}$$
25	19 24	impbii	$$⊢x\subseteq \left\{\varnothing \right\}\leftrightarrow \left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)$$
26	25	abbii	$$⊢\left\{x|x\subseteq \left\{\varnothing \right\}\right\}=\left\{x|\left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)\right\}$$
27		df-pw	$$⊢𝒫\left\{\varnothing \right\}=\left\{x|x\subseteq \left\{\varnothing \right\}\right\}$$
28		dfpr2	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}=\left\{x|\left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)\right\}$$
29	26 27 28	3eqtr4i	$$⊢𝒫\left\{\varnothing \right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$