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 { ⟨ 𝐴 , 𝐵 ⟩ } ⊆ { 𝐴 }