This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpcogend

Description: The most interesting case of the composition of two Cartesian 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		brxp	$⊢ x (A \times B) y \leftrightarrow (x \in A \land y \in B)$
3		brxp	$⊢ y (C \times D) z \leftrightarrow (y \in C \land z \in D)$
4	3	biancomi	$⊢ y (C \times D) z \leftrightarrow (z \in D \land y \in C)$
5	2 4	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))$
6	5	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))$
7		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))$
8	7	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))$
9		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))$
10	6 8 9	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))$
11		ndisj	$⊢ B \cap C \neq \emptyset \leftrightarrow \exists y (y \in B \land y \in C)$
12	1 11	sylib	$⊢ φ \to \exists y (y \in B \land y \in C)$
13	12	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)))$
14	10 13	bitr4id	$⊢ φ \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$