xp11

Description: The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008)

		Ref	Expression
	Assertion	xp11	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (A \times B = C \times D \leftrightarrow (A = C \land B = D))$

Proof

Step	Hyp	Ref	Expression
1		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
2		anidm	$⊢ (A \times B \neq \emptyset \land A \times B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
3		neeq1	$⊢ A \times B = C \times D \to (A \times B \neq \emptyset \leftrightarrow C \times D \neq \emptyset)$
4	3	anbi2d	$⊢ A \times B = C \times D \to ((A \times B \neq \emptyset \land A \times B \neq \emptyset) \leftrightarrow (A \times B \neq \emptyset \land C \times D \neq \emptyset))$
5	2 4	bitr3id	$⊢ A \times B = C \times D \to (A \times B \neq \emptyset \leftrightarrow (A \times B \neq \emptyset \land C \times D \neq \emptyset))$
6		eqimss	$⊢ A \times B = C \times D \to A \times B \subseteq C \times D$
7		ssxpb	$⊢ A \times B \neq \emptyset \to (A \times B \subseteq C \times D \leftrightarrow (A \subseteq C \land B \subseteq D))$
8	6 7	syl5ibcom	$⊢ A \times B = C \times D \to (A \times B \neq \emptyset \to (A \subseteq C \land B \subseteq D))$
9		eqimss2	$⊢ A \times B = C \times D \to C \times D \subseteq A \times B$
10		ssxpb	$⊢ C \times D \neq \emptyset \to (C \times D \subseteq A \times B \leftrightarrow (C \subseteq A \land D \subseteq B))$
11	9 10	syl5ibcom	$⊢ A \times B = C \times D \to (C \times D \neq \emptyset \to (C \subseteq A \land D \subseteq B))$
12	8 11	anim12d	$⊢ A \times B = C \times D \to ((A \times B \neq \emptyset \land C \times D \neq \emptyset) \to ((A \subseteq C \land B \subseteq D) \land (C \subseteq A \land D \subseteq B)))$
13		an4	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \subseteq A \land D \subseteq B)) \leftrightarrow ((A \subseteq C \land C \subseteq A) \land (B \subseteq D \land D \subseteq B))$
14		eqss	$⊢ A = C \leftrightarrow (A \subseteq C \land C \subseteq A)$
15		eqss	$⊢ B = D \leftrightarrow (B \subseteq D \land D \subseteq B)$
16	14 15	anbi12i	$⊢ (A = C \land B = D) \leftrightarrow ((A \subseteq C \land C \subseteq A) \land (B \subseteq D \land D \subseteq B))$
17	13 16	bitr4i	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \subseteq A \land D \subseteq B)) \leftrightarrow (A = C \land B = D)$
18	12 17	imbitrdi	$⊢ A \times B = C \times D \to ((A \times B \neq \emptyset \land C \times D \neq \emptyset) \to (A = C \land B = D))$
19	5 18	sylbid	$⊢ A \times B = C \times D \to (A \times B \neq \emptyset \to (A = C \land B = D))$
20	19	com12	$⊢ A \times B \neq \emptyset \to (A \times B = C \times D \to (A = C \land B = D))$
21	1 20	sylbi	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (A \times B = C \times D \to (A = C \land B = D))$
22		xpeq12	$⊢ (A = C \land B = D) \to A \times B = C \times D$
23	21 22	impbid1	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (A \times B = C \times D \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer

Theorem xp11

Proof