xppss12

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

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

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

Metamath Proof Explorer