Theorem dminxp

Description: Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	dminxp	$$⊢\mathrm{dom}\left(C\cap \left(A\times B\right)\right)=A\leftrightarrow \forall x\in A\exists y\in BxCy$$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}\left(C\cap \left(A\times B\right)\right)=\mathrm{ran}{\left(C\cap \left(A\times B\right)\right)}^{-1}$$
2		cnvin	$$⊢{\left(C\cap \left(A\times B\right)\right)}^{-1}=C^{-1}\cap {\left(A\times B\right)}^{-1}$$
3		cnvxp	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$
4	3	ineq2i	$$⊢C^{-1}\cap {\left(A\times B\right)}^{-1}=C^{-1}\cap \left(B\times A\right)$$
5	2 4	eqtri	$$⊢{\left(C\cap \left(A\times B\right)\right)}^{-1}=C^{-1}\cap \left(B\times A\right)$$
6	5	rneqi	$$⊢\mathrm{ran}{\left(C\cap \left(A\times B\right)\right)}^{-1}=\mathrm{ran}\left(C^{-1}\cap \left(B\times A\right)\right)$$
7	1 6	eqtri	$$⊢\mathrm{dom}\left(C\cap \left(A\times B\right)\right)=\mathrm{ran}\left(C^{-1}\cap \left(B\times A\right)\right)$$
8	7	eqeq1i	$$⊢\mathrm{dom}\left(C\cap \left(A\times B\right)\right)=A\leftrightarrow \mathrm{ran}\left(C^{-1}\cap \left(B\times A\right)\right)=A$$
9		rninxp	$$⊢\mathrm{ran}\left(C^{-1}\cap \left(B\times A\right)\right)=A\leftrightarrow \forall x\in A\exists y\in By{C}^{-1}x$$
10		vex	$$⊢y\in \mathrm{V}$$
11		vex	$$⊢x\in \mathrm{V}$$
12	10 11	brcnv	$$⊢y{C}^{-1}x\leftrightarrow xCy$$
13	12	rexbii	$$⊢\exists y\in By{C}^{-1}x\leftrightarrow \exists y\in BxCy$$
14	13	ralbii	$$⊢\forall x\in A\exists y\in By{C}^{-1}x\leftrightarrow \forall x\in A\exists y\in BxCy$$
15	8 9 14	3bitri	$$⊢\mathrm{dom}\left(C\cap \left(A\times B\right)\right)=A\leftrightarrow \forall x\in A\exists y\in BxCy$$