dmxrn

Description: Domain of the range product. (Contributed by Peter Mazsa, 19-Apr-2020) (Revised by Peter Mazsa, 22-Nov-2025)

		Ref	Expression
	Assertion	dmxrn	$⊢ dom R ⋉ S = dom R \cap dom S$

Step	Hyp	Ref	Expression
1		exdistrv	$⊢ \exists x \exists y (z R x \land z S y) \leftrightarrow (\exists x z R x \land \exists y z S y)$
2	1	abbii	$⊢ \{z \| \exists x \exists y (z R x \land z S y)\} = \{z \| (\exists x z R x \land \exists y z S y)\}$
3		dfxrn2	$⊢ R ⋉ S = {\{⟨⟨x, y⟩, z⟩ \| (z R x \land z S y)\}}^{-1}$
4	3	dmeqi	$⊢ dom R ⋉ S = dom {\{⟨⟨x, y⟩, z⟩ \| (z R x \land z S y)\}}^{-1}$
5		df-rn	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| (z R x \land z S y)\} = dom {\{⟨⟨x, y⟩, z⟩ \| (z R x \land z S y)\}}^{-1}$
6		rnoprab	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| (z R x \land z S y)\} = \{z \| \exists x \exists y (z R x \land z S y)\}$
7	4 5 6	3eqtr2i	$⊢ dom R ⋉ S = \{z \| \exists x \exists y (z R x \land z S y)\}$
8		inab	$⊢ \{z \| \exists x z R x\} \cap \{z \| \exists y z S y\} = \{z \| (\exists x z R x \land \exists y z S y)\}$
9	2 7 8	3eqtr4i	$⊢ dom R ⋉ S = \{z \| \exists x z R x\} \cap \{z \| \exists y z S y\}$
10		df-dm	$⊢ dom R = \{z \| \exists x z R x\}$
11		df-dm	$⊢ dom S = \{z \| \exists y z S y\}$
12	10 11	ineq12i	$⊢ dom R \cap dom S = \{z \| \exists x z R x\} \cap \{z \| \exists y z S y\}$
13	9 12	eqtr4i	$⊢ dom R ⋉ S = dom R \cap dom S$

Metamath Proof Explorer