Metamath Proof Explorer

Theorem dfxrn2

Description: Alternate definition of the range Cartesian product. (Contributed by Peter Mazsa, 20-Feb-2022)

		Ref	Expression
	Assertion	dfxrn2	$⊢ R ⋉ S = {\{⟨⟨x, y⟩, u⟩ \| (u R x \land u S y)\}}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		xrnrel	$⊢ Rel R ⋉ S$
2		dfrel4v	$⊢ Rel R ⋉ S \leftrightarrow R ⋉ S = \{⟨u, z⟩ \| u R ⋉ S z\}$
3	1 2	mpbi	$⊢ R ⋉ S = \{⟨u, z⟩ \| u R ⋉ S z\}$
4		breq2	$⊢ z = ⟨x, y⟩ \to (u R ⋉ S z \leftrightarrow u R ⋉ S ⟨x, y⟩)$
5		brxrn2	$⊢ u \in V \to (u R ⋉ S z \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land u R x \land u S y))$
6	5	elv	$⊢ u R ⋉ S z \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land u R x \land u S y)$
7		brxrn	$⊢ (u \in V \land x \in V \land y \in V) \to (u R ⋉ S ⟨x, y⟩ \leftrightarrow (u R x \land u S y))$
8	7	el3v	$⊢ u R ⋉ S ⟨x, y⟩ \leftrightarrow (u R x \land u S y)$
9	8	anbi2i	$⊢ (z = ⟨x, y⟩ \land u R ⋉ S ⟨x, y⟩) \leftrightarrow (z = ⟨x, y⟩ \land (u R x \land u S y))$
10		3anass	$⊢ (z = ⟨x, y⟩ \land u R x \land u S y) \leftrightarrow (z = ⟨x, y⟩ \land (u R x \land u S y))$
11	9 10	bitr4i	$⊢ (z = ⟨x, y⟩ \land u R ⋉ S ⟨x, y⟩) \leftrightarrow (z = ⟨x, y⟩ \land u R x \land u S y)$
12	11	2exbii	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land u R ⋉ S ⟨x, y⟩) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land u R x \land u S y)$
13	4	copsex2gb	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land u R ⋉ S ⟨x, y⟩) \leftrightarrow (z \in (V \times V) \land u R ⋉ S z)$
14	6 12 13	3bitr2i	$⊢ u R ⋉ S z \leftrightarrow (z \in (V \times V) \land u R ⋉ S z)$
15	14	simplbi	$⊢ u R ⋉ S z \to z \in (V \times V)$
16	4 15	cnvoprab	$⊢ {\{⟨⟨x, y⟩, u⟩ \| u R ⋉ S ⟨x, y⟩\}}^{-1} = \{⟨u, z⟩ \| u R ⋉ S z\}$
17	8	oprabbii	$⊢ \{⟨⟨x, y⟩, u⟩ \| u R ⋉ S ⟨x, y⟩\} = \{⟨⟨x, y⟩, u⟩ \| (u R x \land u S y)\}$
18	17	cnveqi	$⊢ {\{⟨⟨x, y⟩, u⟩ \| u R ⋉ S ⟨x, y⟩\}}^{-1} = {\{⟨⟨x, y⟩, u⟩ \| (u R x \land u S y)\}}^{-1}$
19	3 16 18	3eqtr2i	$⊢ R ⋉ S = {\{⟨⟨x, y⟩, u⟩ \| (u R x \land u S y)\}}^{-1}$