Theorem ssxpb

Description: A Cartesian product subclass relationship is equivalent to the conjunction of the analogous relationships for the factors. (Contributed by NM, 17-Dec-2008)

	Ref	Expression
Assertion	ssxpb	$$⊢A\times B\ne \varnothing \to \left(A\times B\subseteq C\times D\leftrightarrow \left(A\subseteq C\wedge B\subseteq D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpnz	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$
2		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
3	2	adantl	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\to \mathrm{dom}\left(A\times B\right)=A$$
4	1 3	sylbir	$$⊢A\times B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
5	4	adantr	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to \mathrm{dom}\left(A\times B\right)=A$$
6		dmss	$$⊢A\times B\subseteq C\times D\to \mathrm{dom}\left(A\times B\right)\subseteq \mathrm{dom}\left(C\times D\right)$$
7	6	adantl	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to \mathrm{dom}\left(A\times B\right)\subseteq \mathrm{dom}\left(C\times D\right)$$
8	5 7	eqsstrrd	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to A\subseteq \mathrm{dom}\left(C\times D\right)$$
9		dmxpss	$$⊢\mathrm{dom}\left(C\times D\right)\subseteq C$$
10	8 9	sstrdi	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to A\subseteq C$$
11		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$
12	11	adantr	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\to \mathrm{ran}\left(A\times B\right)=B$$
13	1 12	sylbir	$$⊢A\times B\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$
14	13	adantr	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to \mathrm{ran}\left(A\times B\right)=B$$
15		rnss	$$⊢A\times B\subseteq C\times D\to \mathrm{ran}\left(A\times B\right)\subseteq \mathrm{ran}\left(C\times D\right)$$
16	15	adantl	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to \mathrm{ran}\left(A\times B\right)\subseteq \mathrm{ran}\left(C\times D\right)$$
17	14 16	eqsstrrd	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to B\subseteq \mathrm{ran}\left(C\times D\right)$$
18		rnxpss	$$⊢\mathrm{ran}\left(C\times D\right)\subseteq D$$
19	17 18	sstrdi	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to B\subseteq D$$
20	10 19	jca	$$⊢\left(A\times B\ne \varnothing \wedge A\times B\subseteq C\times D\right)\to \left(A\subseteq C\wedge B\subseteq D\right)$$
21	20	ex	$$⊢A\times B\ne \varnothing \to \left(A\times B\subseteq C\times D\to \left(A\subseteq C\wedge B\subseteq D\right)\right)$$
22		xpss12	$$⊢\left(A\subseteq C\wedge B\subseteq D\right)\to A\times B\subseteq C\times D$$
23	21 22	impbid1	$$⊢A\times B\ne \varnothing \to \left(A\times B\subseteq C\times D\leftrightarrow \left(A\subseteq C\wedge B\subseteq D\right)\right)$$