Theorem brimage

Description: Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brimage.1	$$⊢A\in \mathrm{V}$$
	brimage.2	$$⊢B\in \mathrm{V}$$
Assertion	brimage	$$⊢A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\leftrightarrow B=R\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		brimage.1	$$⊢A\in \mathrm{V}$$
2		brimage.2	$$⊢B\in \mathrm{V}$$
3		df-image	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}R=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ R^{-1}\right)\otimes \mathrm{V}\right)\right)$$
4		brxp	$$⊢A\left(\mathrm{V}\times \mathrm{V}\right)B\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5	1 2 4	mpbir2an	$$⊢A\left(\mathrm{V}\times \mathrm{V}\right)B$$
6		vex	$$⊢x\in \mathrm{V}$$
7		vex	$$⊢y\in \mathrm{V}$$
8	6 7	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
9	8	rexbii	$$⊢\exists y\in Ax{R}^{-1}y\leftrightarrow \exists y\in AyRx$$
10	6 1	coep	$$⊢x\left(\mathrm{E}\circ R^{-1}\right)A\leftrightarrow \exists y\in Ax{R}^{-1}y$$
11	6	elima	$$⊢x\in R\left[A\right]\leftrightarrow \exists y\in AyRx$$
12	9 10 11	3bitr4ri	$$⊢x\in R\left[A\right]\leftrightarrow x\left(\mathrm{E}\circ R^{-1}\right)A$$
13	1 2 3 5 12	brtxpsd3	$$⊢A\mathrm{𝖨𝗆𝖺𝗀𝖾}RB\leftrightarrow B=R\left[A\right]$$