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	⊢ dom { { { 𝐴 } } } = { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	opid	⊢ ⟨ 𝑥 , 𝑥 ⟩ = { { 𝑥 } }
3		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4	3	sneqd	⊢ ( 𝑥 = 𝐴 → { { 𝑥 } } = { { 𝐴 } } )
5	2 4	syl5eq	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ = { { 𝐴 } } )
6	5	sneqd	⊢ ( 𝑥 = 𝐴 → { ⟨ 𝑥 , 𝑥 ⟩ } = { { { 𝐴 } } } )
7	6	dmeqd	⊢ ( 𝑥 = 𝐴 → dom { ⟨ 𝑥 , 𝑥 ⟩ } = dom { { { 𝐴 } } } )
8	7 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( dom { ⟨ 𝑥 , 𝑥 ⟩ } = { 𝑥 } ↔ dom { { { 𝐴 } } } = { 𝐴 } ) )
9	1	dmsnop	⊢ dom { ⟨ 𝑥 , 𝑥 ⟩ } = { 𝑥 }
10	8 9	vtoclg	⊢ ( 𝐴 ∈ V → dom { { { 𝐴 } } } = { 𝐴 } )
11		0ex	⊢ ∅ ∈ V
12	11	snid	⊢ ∅ ∈ { ∅ }
13		dmsn0el	⊢ ( ∅ ∈ { ∅ } → dom { { ∅ } } = ∅ )
14	12 13	ax-mp	⊢ dom { { ∅ } } = ∅
15		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
16	15	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
17	16	sneqd	⊢ ( ¬ 𝐴 ∈ V → { { 𝐴 } } = { ∅ } )
18	17	sneqd	⊢ ( ¬ 𝐴 ∈ V → { { { 𝐴 } } } = { { ∅ } } )
19	18	dmeqd	⊢ ( ¬ 𝐴 ∈ V → dom { { { 𝐴 } } } = dom { { ∅ } } )
20	14 19 16	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → dom { { { 𝐴 } } } = { 𝐴 } )
21	10 20	pm2.61i	⊢ dom { { { 𝐴 } } } = { 𝐴 }