Metamath Proof Explorer


Theorem dmxpss

Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007)

Ref Expression
Assertion dmxpss dom ( 𝐴 × 𝐵 ) ⊆ 𝐴

Proof

Step Hyp Ref Expression
1 xpeq2 ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
2 xp0 ( 𝐴 × ∅ ) = ∅
3 1 2 eqtrdi ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
4 3 dmeqd ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) = dom ∅ )
5 dm0 dom ∅ = ∅
6 4 5 eqtrdi ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) = ∅ )
7 0ss ∅ ⊆ 𝐴
8 6 7 eqsstrdi ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
9 dmxp ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
10 eqimss ( dom ( 𝐴 × 𝐵 ) = 𝐴 → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
11 9 10 syl ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
12 8 11 pm2.61ine dom ( 𝐴 × 𝐵 ) ⊆ 𝐴