coxp

Description: Composition with a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025)

		Ref	Expression
	Assertion	coxp	$⊢ A \circ (B \times C) = B \times A [C]$

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel (A \circ (B \times C))$
2		relxp	$⊢ Rel (B \times A [C])$
3		brxp	$⊢ x (B \times C) z \leftrightarrow (x \in B \land z \in C)$
4	3	anbi1i	$⊢ (x (B \times C) z \land z A y) \leftrightarrow ((x \in B \land z \in C) \land z A y)$
5		anass	$⊢ ((x \in B \land z \in C) \land z A y) \leftrightarrow (x \in B \land (z \in C \land z A y))$
6	4 5	bitri	$⊢ (x (B \times C) z \land z A y) \leftrightarrow (x \in B \land (z \in C \land z A y))$
7	6	exbii	$⊢ \exists z (x (B \times C) z \land z A y) \leftrightarrow \exists z (x \in B \land (z \in C \land z A y))$
8		vex	$⊢ x \in V$
9		vex	$⊢ y \in V$
10	8 9	opelco	$⊢ ⟨x, y⟩ \in (A \circ (B \times C)) \leftrightarrow \exists z (x (B \times C) z \land z A y)$
11	9	elima2	$⊢ y \in A [C] \leftrightarrow \exists z (z \in C \land z A y)$
12	11	anbi2i	$⊢ (x \in B \land y \in A [C]) \leftrightarrow (x \in B \land \exists z (z \in C \land z A y))$
13		opelxp	$⊢ ⟨x, y⟩ \in (B \times A [C]) \leftrightarrow (x \in B \land y \in A [C])$
14		19.42v	$⊢ \exists z (x \in B \land (z \in C \land z A y)) \leftrightarrow (x \in B \land \exists z (z \in C \land z A y))$
15	12 13 14	3bitr4i	$⊢ ⟨x, y⟩ \in (B \times A [C]) \leftrightarrow \exists z (x \in B \land (z \in C \land z A y))$
16	7 10 15	3bitr4i	$⊢ ⟨x, y⟩ \in (A \circ (B \times C)) \leftrightarrow ⟨x, y⟩ \in (B \times A [C])$
17	1 2 16	eqrelriiv	$⊢ A \circ (B \times C) = B \times A [C]$

Metamath Proof Explorer