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	$⊢ dom \{\{\{A\}\}\} = \{A\}$

Proof

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

Metamath Proof Explorer

Theorem dmsnsnsn

Proof