Theorem dmsnsnsn

Description: The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	dmsnsnsn	$$⊢\mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	opid	$$⊢⟨x,x⟩=\left\{\left\{x\right\}\right\}$$
3		sneq	$$⊢x=A\to \left\{x\right\}=\left\{A\right\}$$
4	3	sneqd	$$⊢x=A\to \left\{\left\{x\right\}\right\}=\left\{\left\{A\right\}\right\}$$
5	2 4	syl5eq	$$⊢x=A\to ⟨x,x⟩=\left\{\left\{A\right\}\right\}$$
6	5	sneqd	$$⊢x=A\to \left\{⟨x,x⟩\right\}=\left\{\left\{\left\{A\right\}\right\}\right\}$$
7	6	dmeqd	$$⊢x=A\to \mathrm{dom}\left\{⟨x,x⟩\right\}=\mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}$$
8	7 3	eqeq12d	$$⊢x=A\to \left(\mathrm{dom}\left\{⟨x,x⟩\right\}=\left\{x\right\}\leftrightarrow \mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{A\right\}\right)$$
9	1	dmsnop	$$⊢\mathrm{dom}\left\{⟨x,x⟩\right\}=\left\{x\right\}$$
10	8 9	vtoclg	$$⊢A\in \mathrm{V}\to \mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{A\right\}$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12	11	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
13		dmsn0el	$$⊢\varnothing \in \left\{\varnothing \right\}\to \mathrm{dom}\left\{\left\{\varnothing \right\}\right\}=\varnothing$$
14	12 13	ax-mp	$$⊢\mathrm{dom}\left\{\left\{\varnothing \right\}\right\}=\varnothing$$
15		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
16	15	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
17	16	sneqd	$$⊢\neg A\in \mathrm{V}\to \left\{\left\{A\right\}\right\}=\left\{\varnothing \right\}$$
18	17	sneqd	$$⊢\neg A\in \mathrm{V}\to \left\{\left\{\left\{A\right\}\right\}\right\}=\left\{\left\{\varnothing \right\}\right\}$$
19	18	dmeqd	$$⊢\neg A\in \mathrm{V}\to \mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\mathrm{dom}\left\{\left\{\varnothing \right\}\right\}$$
20	14 19 16	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to \mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{A\right\}$$
21	10 20	pm2.61i	$$⊢\mathrm{dom}\left\{\left\{\left\{A\right\}\right\}\right\}=\left\{A\right\}$$