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 ( A X. B ) C_ A

Proof

Step Hyp Ref Expression
1 xpeq2
 |-  ( B = (/) -> ( A X. B ) = ( A X. (/) ) )
2 xp0
 |-  ( A X. (/) ) = (/)
3 1 2 eqtrdi
 |-  ( B = (/) -> ( A X. B ) = (/) )
4 3 dmeqd
 |-  ( B = (/) -> dom ( A X. B ) = dom (/) )
5 dm0
 |-  dom (/) = (/)
6 4 5 eqtrdi
 |-  ( B = (/) -> dom ( A X. B ) = (/) )
7 0ss
 |-  (/) C_ A
8 6 7 eqsstrdi
 |-  ( B = (/) -> dom ( A X. B ) C_ A )
9 dmxp
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
10 eqimss
 |-  ( dom ( A X. B ) = A -> dom ( A X. B ) C_ A )
11 9 10 syl
 |-  ( B =/= (/) -> dom ( A X. B ) C_ A )
12 8 11 pm2.61ine
 |-  dom ( A X. B ) C_ A