Definition df-img

Description: Define the image function. See brimg for its value. (Contributed by Scott Fenton, 12-Apr-2014)

	Ref	Expression
Assertion	df-img	$$⊢\mathrm{𝖨𝗆𝗀}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({\left(2^{nd}\circ 1^{st}\right)\upharpoonright }_{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}\right)\circ \mathrm{𝖢𝖺𝗋𝗍}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cimg	$$class\mathrm{𝖨𝗆𝗀}$$
1		c2nd	$$class{2}^{nd}$$
2		c1st	$$class{1}^{st}$$
3	1 2	ccom	$$class\left(2^{nd}\circ 1^{st}\right)$$
4		cvv	$$class\mathrm{V}$$
5	4 4	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
6	2 5	cres	$$class\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
7	3 6	cres	$$class\left({\left(2^{nd}\circ 1^{st}\right)\upharpoonright }_{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}\right)$$
8	7	cimage	$$class\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({\left(2^{nd}\circ 1^{st}\right)\upharpoonright }_{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}\right)$$
9		ccart	$$class\mathrm{𝖢𝖺𝗋𝗍}$$
10	8 9	ccom	$$class\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({\left(2^{nd}\circ 1^{st}\right)\upharpoonright }_{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}\right)\circ \mathrm{𝖢𝖺𝗋𝗍}\right)$$
11	0 10	wceq	$$wff\mathrm{𝖨𝗆𝗀}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({\left(2^{nd}\circ 1^{st}\right)\upharpoonright }_{\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}\right)\circ \mathrm{𝖢𝖺𝗋𝗍}$$