Theorem xpss12

Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of Suppes p. 52. (Contributed by NM, 26-Aug-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	xpss12	$$⊢\left(A\subseteq B\wedge C\subseteq D\right)\to A\times C\subseteq B\times D$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢A\subseteq B\to \left(x\in A\to x\in B\right)$$
2		ssel	$$⊢C\subseteq D\to \left(y\in C\to y\in D\right)$$
3	1 2	im2anan9	$$⊢\left(A\subseteq B\wedge C\subseteq D\right)\to \left(\left(x\in A\wedge y\in C\right)\to \left(x\in B\wedge y\in D\right)\right)$$
4	3	ssopab2dv	$$⊢\left(A\subseteq B\wedge C\subseteq D\right)\to \left\{⟨x,y⟩|\left(x\in A\wedge y\in C\right)\right\}\subseteq \left\{⟨x,y⟩|\left(x\in B\wedge y\in D\right)\right\}$$
5		df-xp	$$⊢A\times C=\left\{⟨x,y⟩|\left(x\in A\wedge y\in C\right)\right\}$$
6		df-xp	$$⊢B\times D=\left\{⟨x,y⟩|\left(x\in B\wedge y\in D\right)\right\}$$
7	4 5 6	3sstr4g	$$⊢\left(A\subseteq B\wedge C\subseteq D\right)\to A\times C\subseteq B\times D$$