Theorem pwsnOLD

Description: Obsolete version of pwsn as of 14-Apr-2024. Note that the proof is essentially the same once one inlines sssn in the proof of pwsn . (Contributed by NM, 5-Jun-2006) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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