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 domA×BA

Proof

Step Hyp Ref Expression
1 xpeq2 B=A×B=A×
2 xp0 A×=
3 1 2 eqtrdi B=A×B=
4 3 dmeqd B=domA×B=dom
5 dm0 dom=
6 4 5 eqtrdi B=domA×B=
7 0ss A
8 6 7 eqsstrdi B=domA×BA
9 dmxp BdomA×B=A
10 eqimss domA×B=AdomA×BA
11 9 10 syl BdomA×BA
12 8 11 pm2.61ine domA×BA