inxpxrn

Description: Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020)

		Ref	Expression
	Assertion	inxpxrn	$⊢ (R \cap (A \times B)) ⋉ (S \cap (A \times C)) = R ⋉ S \cap (A \times (B \times C))$

Proof

Step	Hyp	Ref	Expression
1		xrnrel	$⊢ Rel (R \cap (A \times B)) ⋉ (S \cap (A \times C))$
2		relinxp	$⊢ Rel (R ⋉ S \cap (A \times (B \times C)))$
3		brxrn2	$⊢ u \in V \to (u R ⋉ S x \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z))$
4	3	elv	$⊢ u R ⋉ S x \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z)$
5	4	anbi2i	$⊢ (u \in A \land u R ⋉ S x) \leftrightarrow (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z))$
6	5	anbi2i	$⊢ (x \in (B \times C) \land (u \in A \land u R ⋉ S x)) \leftrightarrow (x \in (B \times C) \land (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z)))$
7		xrninxp2	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$
8	7	brabidgaw	$⊢ u (R ⋉ S \cap (A \times (B \times C))) x \leftrightarrow (x \in (B \times C) \land (u \in A \land u R ⋉ S x))$
9		brxrn2	$⊢ u \in V \to (u (R \cap (A \times B)) ⋉ (S \cap (A \times C)) x \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z))$
10	9	elv	$⊢ u (R \cap (A \times B)) ⋉ (S \cap (A \times C)) x \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)$
11		3anass	$⊢ (x = ⟨y, z⟩ \land u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z) \leftrightarrow (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z))$
12	11	2exbii	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z))$
13		brinxp2	$⊢ u (R \cap (A \times B)) y \leftrightarrow ((u \in A \land y \in B) \land u R y)$
14		brinxp2	$⊢ u (S \cap (A \times C)) z \leftrightarrow ((u \in A \land z \in C) \land u S z)$
15	13 14	anbi12i	$⊢ (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z) \leftrightarrow (((u \in A \land y \in B) \land u R y) \land ((u \in A \land z \in C) \land u S z))$
16		anan	$⊢ (((u \in A \land y \in B) \land u R y) \land ((u \in A \land z \in C) \land u S z)) \leftrightarrow ((y \in B \land z \in C) \land (u \in A \land (u R y \land u S z)))$
17	15 16	bitri	$⊢ (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z) \leftrightarrow ((y \in B \land z \in C) \land (u \in A \land (u R y \land u S z)))$
18	17	anbi2i	$⊢ (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow (x = ⟨y, z⟩ \land ((y \in B \land z \in C) \land (u \in A \land (u R y \land u S z))))$
19		anass	$⊢ ((x = ⟨y, z⟩ \land (y \in B \land z \in C)) \land (u \in A \land (u R y \land u S z))) \leftrightarrow (x = ⟨y, z⟩ \land ((y \in B \land z \in C) \land (u \in A \land (u R y \land u S z))))$
20		eqelb	$⊢ (x = ⟨y, z⟩ \land x \in (B \times C)) \leftrightarrow (x = ⟨y, z⟩ \land ⟨y, z⟩ \in (B \times C))$
21		opelxp	$⊢ ⟨y, z⟩ \in (B \times C) \leftrightarrow (y \in B \land z \in C)$
22	21	anbi2i	$⊢ (x = ⟨y, z⟩ \land ⟨y, z⟩ \in (B \times C)) \leftrightarrow (x = ⟨y, z⟩ \land (y \in B \land z \in C))$
23	20 22	bitr2i	$⊢ (x = ⟨y, z⟩ \land (y \in B \land z \in C)) \leftrightarrow (x = ⟨y, z⟩ \land x \in (B \times C))$
24	23	anbi1i	$⊢ ((x = ⟨y, z⟩ \land (y \in B \land z \in C)) \land (u \in A \land (u R y \land u S z))) \leftrightarrow ((x = ⟨y, z⟩ \land x \in (B \times C)) \land (u \in A \land (u R y \land u S z)))$
25	18 19 24	3bitr2i	$⊢ (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow ((x = ⟨y, z⟩ \land x \in (B \times C)) \land (u \in A \land (u R y \land u S z)))$
26		ancom	$⊢ (x = ⟨y, z⟩ \land x \in (B \times C)) \leftrightarrow (x \in (B \times C) \land x = ⟨y, z⟩)$
27	26	anbi1i	$⊢ ((x = ⟨y, z⟩ \land x \in (B \times C)) \land (u \in A \land (u R y \land u S z))) \leftrightarrow ((x \in (B \times C) \land x = ⟨y, z⟩) \land (u \in A \land (u R y \land u S z)))$
28		anass	$⊢ ((x \in (B \times C) \land x = ⟨y, z⟩) \land (u \in A \land (u R y \land u S z))) \leftrightarrow (x \in (B \times C) \land (x = ⟨y, z⟩ \land (u \in A \land (u R y \land u S z))))$
29	25 27 28	3bitri	$⊢ (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow (x \in (B \times C) \land (x = ⟨y, z⟩ \land (u \in A \land (u R y \land u S z))))$
30		an12	$⊢ (x = ⟨y, z⟩ \land (u \in A \land (u R y \land u S z))) \leftrightarrow (u \in A \land (x = ⟨y, z⟩ \land (u R y \land u S z)))$
31		3anass	$⊢ (x = ⟨y, z⟩ \land u R y \land u S z) \leftrightarrow (x = ⟨y, z⟩ \land (u R y \land u S z))$
32	31	anbi2i	$⊢ (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)) \leftrightarrow (u \in A \land (x = ⟨y, z⟩ \land (u R y \land u S z)))$
33	30 32	bitr4i	$⊢ (x = ⟨y, z⟩ \land (u \in A \land (u R y \land u S z))) \leftrightarrow (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z))$
34	33	anbi2i	$⊢ (x \in (B \times C) \land (x = ⟨y, z⟩ \land (u \in A \land (u R y \land u S z)))) \leftrightarrow (x \in (B \times C) \land (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)))$
35	29 34	bitri	$⊢ (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow (x \in (B \times C) \land (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)))$
36	35	2exbii	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow \exists y \exists z (x \in (B \times C) \land (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)))$
37		19.42vv	$⊢ \exists y \exists z (x \in (B \times C) \land (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z))) \leftrightarrow (x \in (B \times C) \land \exists y \exists z (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)))$
38		19.42vv	$⊢ \exists y \exists z (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z)) \leftrightarrow (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z))$
39	38	anbi2i	$⊢ (x \in (B \times C) \land \exists y \exists z (u \in A \land (x = ⟨y, z⟩ \land u R y \land u S z))) \leftrightarrow (x \in (B \times C) \land (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z)))$
40	36 37 39	3bitri	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land (u (R \cap (A \times B)) y \land u (S \cap (A \times C)) z)) \leftrightarrow (x \in (B \times C) \land (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z)))$
41	10 12 40	3bitri	$⊢ u (R \cap (A \times B)) ⋉ (S \cap (A \times C)) x \leftrightarrow (x \in (B \times C) \land (u \in A \land \exists y \exists z (x = ⟨y, z⟩ \land u R y \land u S z)))$
42	6 8 41	3bitr4ri	$⊢ u (R \cap (A \times B)) ⋉ (S \cap (A \times C)) x \leftrightarrow u (R ⋉ S \cap (A \times (B \times C))) x$
43	1 2 42	eqbrriv	$⊢ (R \cap (A \times B)) ⋉ (S \cap (A \times C)) = R ⋉ S \cap (A \times (B \times C))$

Metamath Proof Explorer

Theorem inxpxrn

Proof