Theorem rninxp

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step	Hyp	Ref	Expression
1		dfss3	$$⊢B\subseteq \mathrm{ran}\left({C\upharpoonright }_A\right)\leftrightarrow \forall y\in By\in \mathrm{ran}\left({C\upharpoonright }_A\right)$$
2		ssrnres	$$⊢B\subseteq \mathrm{ran}\left({C\upharpoonright }_A\right)\leftrightarrow \mathrm{ran}\left(C\cap \left(A\times B\right)\right)=B$$
3		df-ima	$$⊢C\left[A\right]=\mathrm{ran}\left({C\upharpoonright }_A\right)$$
4	3	eleq2i	$$⊢y\in C\left[A\right]\leftrightarrow y\in \mathrm{ran}\left({C\upharpoonright }_A\right)$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	elima	$$⊢y\in C\left[A\right]\leftrightarrow \exists x\in AxCy$$
7	4 6	bitr3i	$$⊢y\in \mathrm{ran}\left({C\upharpoonright }_A\right)\leftrightarrow \exists x\in AxCy$$
8	7	ralbii	$$⊢\forall y\in By\in \mathrm{ran}\left({C\upharpoonright }_A\right)\leftrightarrow \forall y\in B\exists x\in AxCy$$
9	1 2 8	3bitr3i	$$⊢\mathrm{ran}\left(C\cap \left(A\times B\right)\right)=B\leftrightarrow \forall y\in B\exists x\in AxCy$$