xpco2

Description: Composition of a Cartesian product with a function. (Contributed by Zhi Wang, 25-Nov-2025)

		Ref	Expression
	Assertion	xpco2	$⊢ F : A ⟶ B \to (B \times C) \circ F = A \times C$

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel ((B \times C) \circ F)$
2		relxp	$⊢ Rel (A \times C)$
3		vex	$⊢ x \in V$
4		vex	$⊢ z \in V$
5	3 4	breldm	$⊢ x F z \to x \in dom F$
6	5	ad2antrl	$⊢ (F : A ⟶ B \land (x F z \land z (B \times C) y)) \to x \in dom F$
7		fdm	$⊢ F : A ⟶ B \to dom F = A$
8	7	adantr	$⊢ (F : A ⟶ B \land (x F z \land z (B \times C) y)) \to dom F = A$
9	6 8	eleqtrd	$⊢ (F : A ⟶ B \land (x F z \land z (B \times C) y)) \to x \in A$
10		brxp	$⊢ z (B \times C) y \leftrightarrow (z \in B \land y \in C)$
11	10	simprbi	$⊢ z (B \times C) y \to y \in C$
12	11	ad2antll	$⊢ (F : A ⟶ B \land (x F z \land z (B \times C) y)) \to y \in C$
13	9 12	jca	$⊢ (F : A ⟶ B \land (x F z \land z (B \times C) y)) \to (x \in A \land y \in C)$
14	13	ex	$⊢ F : A ⟶ B \to ((x F z \land z (B \times C) y) \to (x \in A \land y \in C))$
15	14	exlimdv	$⊢ F : A ⟶ B \to (\exists z (x F z \land z (B \times C) y) \to (x \in A \land y \in C))$
16	15	imp	$⊢ (F : A ⟶ B \land \exists z (x F z \land z (B \times C) y)) \to (x \in A \land y \in C)$
17		ffvelcdm	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
18	17	adantrr	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to F (x) \in B$
19		ffvbr	$⊢ (F : A ⟶ B \land x \in A) \to x F F (x)$
20	19	adantrr	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to x F F (x)$
21		simprr	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to y \in C$
22		brxp	$⊢ F (x) (B \times C) y \leftrightarrow (F (x) \in B \land y \in C)$
23	18 21 22	sylanbrc	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to F (x) (B \times C) y$
24	20 23	jca	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to (x F F (x) \land F (x) (B \times C) y)$
25		breq2	$⊢ z = F (x) \to (x F z \leftrightarrow x F F (x))$
26		breq1	$⊢ z = F (x) \to (z (B \times C) y \leftrightarrow F (x) (B \times C) y)$
27	25 26	anbi12d	$⊢ z = F (x) \to ((x F z \land z (B \times C) y) \leftrightarrow (x F F (x) \land F (x) (B \times C) y))$
28	18 24 27	spcedv	$⊢ (F : A ⟶ B \land (x \in A \land y \in C)) \to \exists z (x F z \land z (B \times C) y)$
29	16 28	impbida	$⊢ F : A ⟶ B \to (\exists z (x F z \land z (B \times C) y) \leftrightarrow (x \in A \land y \in C))$
30		vex	$⊢ y \in V$
31	3 30	brco	$⊢ x ((B \times C) \circ F) y \leftrightarrow \exists z (x F z \land z (B \times C) y)$
32		brxp	$⊢ x (A \times C) y \leftrightarrow (x \in A \land y \in C)$
33	29 31 32	3bitr4g	$⊢ F : A ⟶ B \to (x ((B \times C) \circ F) y \leftrightarrow x (A \times C) y)$
34	1 2 33	eqbrrdiv	$⊢ F : A ⟶ B \to (B \times C) \circ F = A \times C$

Metamath Proof Explorer

Theorem xpco2

Proof