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 \times B) \subseteq A$

Step	Hyp	Ref	Expression
1		xpeq2	$⊢ B = \emptyset \to A \times B = A \times \emptyset$
2		xp0	$⊢ A \times \emptyset = \emptyset$
3	1 2	eqtrdi	$⊢ B = \emptyset \to A \times B = \emptyset$
4	3	dmeqd	$⊢ B = \emptyset \to dom (A \times B) = dom \emptyset$
5		dm0	$⊢ dom \emptyset = \emptyset$
6	4 5	eqtrdi	$⊢ B = \emptyset \to dom (A \times B) = \emptyset$
7		0ss	$⊢ \emptyset \subseteq A$
8	6 7	eqsstrdi	$⊢ B = \emptyset \to dom (A \times B) \subseteq A$
9		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
10		eqimss	$⊢ dom (A \times B) = A \to dom (A \times B) \subseteq A$
11	9 10	syl	$⊢ B \neq \emptyset \to dom (A \times B) \subseteq A$
12	8 11	pm2.61ine	$⊢ dom (A \times B) \subseteq A$

Metamath Proof Explorer