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 syl6eq 
 |-  ( B = (/) -> ( A X. B ) = (/) )
4 3 dmeqd 
 |-  ( B = (/) -> dom ( A X. B ) = dom (/) )
5 dm0 
 |-  dom (/) = (/)
6 4 5 syl6eq 
 |-  ( 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