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

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 opid ⊢ ⟨ 𝑥 , 𝑥 ⟩ = { { 𝑥 } }
3 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4 3 sneqd ⊢ ( 𝑥 = 𝐴 → { { 𝑥 } } = { { 𝐴 } } )
5 2 4 eqtrid ⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑥 ⟩ = { { 𝐴 } } )
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 { { { 𝐴 } } } = { 𝐴 }