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

Metamath Proof Explorer

Theorem xrninxp

Description: Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020)

		Ref	Expression
	Assertion	xrninxp	$⊢ R ⋉ S \cap (A \times (B \times C)) = {\{⟨⟨y, z⟩, u⟩ \| ((y \in B \land z \in C) \land (u \in A \land u R ⋉ S ⟨y, z⟩))\}}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		inxp2	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| ((u \in A \land x \in (B \times C)) \land u R ⋉ S x)\}$
2		df-3an	$⊢ (u \in A \land x \in (B \times C) \land u R ⋉ S x) \leftrightarrow ((u \in A \land x \in (B \times C)) \land u R ⋉ S x)$
3		3anan12	$⊢ (u \in A \land x \in (B \times C) \land u R ⋉ S x) \leftrightarrow (x \in (B \times C) \land (u \in A \land u R ⋉ S x))$
4	2 3	bitr3i	$⊢ ((u \in A \land x \in (B \times C)) \land u R ⋉ S x) \leftrightarrow (x \in (B \times C) \land (u \in A \land u R ⋉ S x))$
5	4	opabbii	$⊢ \{⟨u, x⟩ \| ((u \in A \land x \in (B \times C)) \land u R ⋉ S x)\} = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$
6	1 5	eqtri	$⊢ R ⋉ S \cap (A \times (B \times C)) = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$
7		cnvopab	$⊢ {\{⟨x, u⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}}^{-1} = \{⟨u, x⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}$
8		breq2	$⊢ x = ⟨y, z⟩ \to (u R ⋉ S x \leftrightarrow u R ⋉ S ⟨y, z⟩)$
9	8	anbi2d	$⊢ x = ⟨y, z⟩ \to ((u \in A \land u R ⋉ S x) \leftrightarrow (u \in A \land u R ⋉ S ⟨y, z⟩))$
10	9	dfoprab4	$⊢ \{⟨x, u⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\} = \{⟨⟨y, z⟩, u⟩ \| ((y \in B \land z \in C) \land (u \in A \land u R ⋉ S ⟨y, z⟩))\}$
11	10	cnveqi	$⊢ {\{⟨x, u⟩ \| (x \in (B \times C) \land (u \in A \land u R ⋉ S x))\}}^{-1} = {\{⟨⟨y, z⟩, u⟩ \| ((y \in B \land z \in C) \land (u \in A \land u R ⋉ S ⟨y, z⟩))\}}^{-1}$
12	6 7 11	3eqtr2i	$⊢ R ⋉ S \cap (A \times (B \times C)) = {\{⟨⟨y, z⟩, u⟩ \| ((y \in B \land z \in C) \land (u \in A \land u R ⋉ S ⟨y, z⟩))\}}^{-1}$