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

Metamath Proof Explorer

Theorem xpco

Description: Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017)

		Ref	Expression
	Assertion	xpco	$⊢ B \neq \emptyset \to (B \times C) \circ (A \times B) = A \times C$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
2	1	biimpi	$⊢ B \neq \emptyset \to \exists y y \in B$
3	2	biantrurd	$⊢ B \neq \emptyset \to ((x \in A \land z \in C) \leftrightarrow (\exists y y \in B \land (x \in A \land z \in C)))$
4		ancom	$⊢ (x \in A \land y \in B) \leftrightarrow (y \in B \land x \in A)$
5	4	anbi1i	$⊢ ((x \in A \land y \in B) \land (y \in B \land z \in C)) \leftrightarrow ((y \in B \land x \in A) \land (y \in B \land z \in C))$
6		brxp	$⊢ x (A \times B) y \leftrightarrow (x \in A \land y \in B)$
7		brxp	$⊢ y (B \times C) z \leftrightarrow (y \in B \land z \in C)$
8	6 7	anbi12i	$⊢ (x (A \times B) y \land y (B \times C) z) \leftrightarrow ((x \in A \land y \in B) \land (y \in B \land z \in C))$
9		anandi	$⊢ (y \in B \land (x \in A \land z \in C)) \leftrightarrow ((y \in B \land x \in A) \land (y \in B \land z \in C))$
10	5 8 9	3bitr4i	$⊢ (x (A \times B) y \land y (B \times C) z) \leftrightarrow (y \in B \land (x \in A \land z \in C))$
11	10	exbii	$⊢ \exists y (x (A \times B) y \land y (B \times C) z) \leftrightarrow \exists y (y \in B \land (x \in A \land z \in C))$
12		19.41v	$⊢ \exists y (y \in B \land (x \in A \land z \in C)) \leftrightarrow (\exists y y \in B \land (x \in A \land z \in C))$
13	11 12	bitr2i	$⊢ (\exists y y \in B \land (x \in A \land z \in C)) \leftrightarrow \exists y (x (A \times B) y \land y (B \times C) z)$
14	3 13	bitr2di	$⊢ B \neq \emptyset \to (\exists y (x (A \times B) y \land y (B \times C) z) \leftrightarrow (x \in A \land z \in C))$
15	14	opabbidv	$⊢ B \neq \emptyset \to \{⟨x, z⟩ \| \exists y (x (A \times B) y \land y (B \times C) z)\} = \{⟨x, z⟩ \| (x \in A \land z \in C)\}$
16		df-co	$⊢ (B \times C) \circ (A \times B) = \{⟨x, z⟩ \| \exists y (x (A \times B) y \land y (B \times C) z)\}$
17		df-xp	$⊢ A \times C = \{⟨x, z⟩ \| (x \in A \land z \in C)\}$
18	15 16 17	3eqtr4g	$⊢ B \neq \emptyset \to (B \times C) \circ (A \times B) = A \times C$