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

Metamath Proof Explorer

Theorem dmsnopss

Description: The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on B ). (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion dmsnopss dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }

Proof

Step Hyp Ref Expression
1 dmsnopg ⊢ ( 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
2 eqimss ⊢ ( dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
3 1 2 syl ⊢ ( 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
4 opprc2 ⊢ ( ¬ 𝐵 ∈ V → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
5 4 sneqd ⊢ ( ¬ 𝐵 ∈ V → { ⟨ 𝐴 , 𝐵 ⟩ } = { ∅ } )
6 5 dmeqd ⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = dom { ∅ } )
7 dmsn0 ⊢ dom { ∅ } = ∅
8 6 7 eqtrdi ⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ )
9 0ss ⊢ ∅ ⊆ { 𝐴 }
10 8 9 eqsstrdi ⊢ ( ¬ 𝐵 ∈ V → dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 } )
11 3 10 pm2.61i ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }