This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { { { A } } } = { A }

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 opid 
 |-  <. x , x >. = { { x } }
3 sneq 
 |-  ( x = A -> { x } = { A } )
4 3 sneqd 
 |-  ( x = A -> { { x } } = { { A } } )
5 2 4 eqtrid 
 |-  ( x = A -> <. x , x >. = { { A } } )
6 5 sneqd 
 |-  ( x = A -> { <. x , x >. } = { { { A } } } )
7 6 dmeqd 
 |-  ( x = A -> dom { <. x , x >. } = dom { { { A } } } )
8 7 3 eqeq12d 
 |-  ( x = A -> ( dom { <. x , x >. } = { x } <-> dom { { { A } } } = { A } ) )
9 1 dmsnop 
 |-  dom { <. x , x >. } = { x }
10 8 9 vtoclg 
 |-  ( A e. _V -> dom { { { A } } } = { A } )
11 0ex 
 |-  (/) e. _V
12 11 snid 
 |-  (/) e. { (/) }
13 dmsn0el 
 |-  ( (/) e. { (/) } -> dom { { (/) } } = (/) )
14 12 13 ax-mp 
 |-  dom { { (/) } } = (/)
15 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
16 15 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
17 16 sneqd 
 |-  ( -. A e. _V -> { { A } } = { (/) } )
18 17 sneqd 
 |-  ( -. A e. _V -> { { { A } } } = { { (/) } } )
19 18 dmeqd 
 |-  ( -. A e. _V -> dom { { { A } } } = dom { { (/) } } )
20 14 19 16 3eqtr4a 
 |-  ( -. A e. _V -> dom { { { A } } } = { A } )
21 10 20 pm2.61i 
 |-  dom { { { A } } } = { A }