Definition df-image

Description: Define the image functor. This function takes a set A to a function x |-> ( A " x ) , providing that the latter exists. See imageval for the derivation. (Contributed by Scott Fenton, 27-Mar-2014)

	Ref	Expression
Assertion	df-image	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}A=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cimage	$$class\mathrm{𝖨𝗆𝖺𝗀𝖾}A$$
2		cvv	$$class\mathrm{V}$$
3	2 2	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
4		cep	$$class\mathrm{E}$$
5	2 4	ctxp	$$class\left(\mathrm{V}\otimes \mathrm{E}\right)$$
6	0	ccnv	$$class{A}^{-1}$$
7	4 6	ccom	$$class\left(\mathrm{E}\circ A^{-1}\right)$$
8	7 2	ctxp	$$class\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)$$
9	5 8	csymdif	$$class\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)\right)$$
10	9	crn	$$class\mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)\right)$$
11	3 10	cdif	$$class\left(\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)\right)\right)$$
12	1 11	wceq	$$wff\mathrm{𝖨𝗆𝖺𝗀𝖾}A=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\mathrm{E}\circ A^{-1}\right)\otimes \mathrm{V}\right)\right)$$