Theorem xppss12

Description: Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022)

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

Proof

Step	Hyp	Ref	Expression
1		pssss	$$⊢A\subset B\to A\subseteq B$$
2		pssss	$$⊢C\subset D\to C\subseteq D$$
3		xpss12	$$⊢\left(A\subseteq B\wedge C\subseteq D\right)\to A\times C\subseteq B\times D$$
4	1 2 3	syl2an	$$⊢\left(A\subset B\wedge C\subset D\right)\to A\times C\subseteq B\times D$$
5		simpl	$$⊢\left(A\subset B\wedge C\subset D\right)\to A\subset B$$
6		pssne	$$⊢A\subset B\to A\ne B$$
7	6	necomd	$$⊢A\subset B\to B\ne A$$
8		neneq	$$⊢B\ne A\to \neg B=A$$
9	8	intnanrd	$$⊢B\ne A\to \neg \left(B=A\wedge D=C\right)$$
10	5 7 9	3syl	$$⊢\left(A\subset B\wedge C\subset D\right)\to \neg \left(B=A\wedge D=C\right)$$
11		pssn0	$$⊢A\subset B\to B\ne \varnothing$$
12		pssn0	$$⊢C\subset D\to D\ne \varnothing$$
13		xp11	$$⊢\left(B\ne \varnothing \wedge D\ne \varnothing \right)\to \left(B\times D=A\times C\leftrightarrow \left(B=A\wedge D=C\right)\right)$$
14	11 12 13	syl2an	$$⊢\left(A\subset B\wedge C\subset D\right)\to \left(B\times D=A\times C\leftrightarrow \left(B=A\wedge D=C\right)\right)$$
15	10 14	mtbird	$$⊢\left(A\subset B\wedge C\subset D\right)\to \neg B\times D=A\times C$$
16		neqne	$$⊢\neg B\times D=A\times C\to B\times D\ne A\times C$$
17	16	necomd	$$⊢\neg B\times D=A\times C\to A\times C\ne B\times D$$
18	15 17	syl	$$⊢\left(A\subset B\wedge C\subset D\right)\to A\times C\ne B\times D$$
19		df-pss	$$⊢A\times C\subset B\times D\leftrightarrow \left(A\times C\subseteq B\times D\wedge A\times C\ne B\times D\right)$$
20	4 18 19	sylanbrc	$$⊢\left(A\subset B\wedge C\subset D\right)\to A\times C\subset B\times D$$