Metamath Proof Explorer

Theorem xpcogend

Description: The most interesting case of the composition of two cross products. (Contributed by RP, 24-Dec-2019)

		Ref	Expression
	Hypothesis	xpcogend.1	$⊢ φ \to B \cap C \neq \emptyset$
	Assertion	xpcogend	$⊢ φ \to (C \times D) \circ (A \times B) = A \times D$

Proof

Step	Hyp	Ref	Expression
1		xpcogend.1	$⊢ φ \to B \cap C \neq \emptyset$
2		ndisj	$⊢ B \cap C \neq \emptyset \leftrightarrow \exists y (y \in B \land y \in C)$
3	1 2	sylib	$⊢ φ \to \exists y (y \in B \land y \in C)$
4	3	biantrud	$⊢ φ \to ((x \in A \land z \in D) \leftrightarrow ((x \in A \land z \in D) \land \exists y (y \in B \land y \in C)))$
5		brxp	$⊢ x (A \times B) y \leftrightarrow (x \in A \land y \in B)$
6		brxp	$⊢ y (C \times D) z \leftrightarrow (y \in C \land z \in D)$
7	6	biancomi	$⊢ y (C \times D) z \leftrightarrow (z \in D \land y \in C)$
8	5 7	anbi12i	$⊢ (x (A \times B) y \land y (C \times D) z) \leftrightarrow ((x \in A \land y \in B) \land (z \in D \land y \in C))$
9	8	exbii	$⊢ \exists y (x (A \times B) y \land y (C \times D) z) \leftrightarrow \exists y ((x \in A \land y \in B) \land (z \in D \land y \in C))$
10		an4	$⊢ ((x \in A \land y \in B) \land (z \in D \land y \in C)) \leftrightarrow ((x \in A \land z \in D) \land (y \in B \land y \in C))$
11	10	exbii	$⊢ \exists y ((x \in A \land y \in B) \land (z \in D \land y \in C)) \leftrightarrow \exists y ((x \in A \land z \in D) \land (y \in B \land y \in C))$
12		19.42v	$⊢ \exists y ((x \in A \land z \in D) \land (y \in B \land y \in C)) \leftrightarrow ((x \in A \land z \in D) \land \exists y (y \in B \land y \in C))$
13	9 11 12	3bitri	$⊢ \exists y (x (A \times B) y \land y (C \times D) z) \leftrightarrow ((x \in A \land z \in D) \land \exists y (y \in B \land y \in C))$
14	4 13	syl6rbbr	$⊢ φ \to (\exists y (x (A \times B) y \land y (C \times D) z) \leftrightarrow (x \in A \land z \in D))$
15	14	opabbidv	$⊢ φ \to \{⟨x, z⟩ \| \exists y (x (A \times B) y \land y (C \times D) z)\} = \{⟨x, z⟩ \| (x \in A \land z \in D)\}$
16		df-co	$⊢ (C \times D) \circ (A \times B) = \{⟨x, z⟩ \| \exists y (x (A \times B) y \land y (C \times D) z)\}$
17		df-xp	$⊢ A \times D = \{⟨x, z⟩ \| (x \in A \land z \in D)\}$
18	15 16 17	3eqtr4g	$⊢ φ \to (C \times D) \circ (A \times B) = A \times D$