Definition df-funs

Description: Define the class of all functions. See elfuns for membership. (Contributed by Scott Fenton, 18-Feb-2013)

	Ref	Expression
Assertion	df-funs	$$⊢\mathrm{𝖥𝗎𝗇𝗌}=𝒫\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{𝖥𝗂𝗑}\left(\mathrm{E}\circ \left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuns	$$class\mathrm{𝖥𝗎𝗇𝗌}$$
1		cvv	$$class\mathrm{V}$$
2	1 1	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	cpw	$$class𝒫\left(\mathrm{V}\times \mathrm{V}\right)$$
4		cep	$$class\mathrm{E}$$
5		c1st	$$class{1}^{st}$$
6		cid	$$class\mathrm{I}$$
7	1 6	cdif	$$class\left(\mathrm{V}\setminus \mathrm{I}\right)$$
8		c2nd	$$class{2}^{nd}$$
9	7 8	ccom	$$class\left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)$$
10	5 9	ctxp	$$class\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)$$
11	4	ccnv	$$class{\mathrm{E}}^{-1}$$
12	10 11	ccom	$$class\left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)$$
13	4 12	ccom	$$class\left(\mathrm{E}\circ \left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)\right)$$
14	13	cfix	$$class\mathrm{𝖥𝗂𝗑}\left(\mathrm{E}\circ \left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)\right)$$
15	3 14	cdif	$$class\left(𝒫\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{𝖥𝗂𝗑}\left(\mathrm{E}\circ \left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)\right)\right)$$
16	0 15	wceq	$$wff\mathrm{𝖥𝗎𝗇𝗌}=𝒫\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{𝖥𝗂𝗑}\left(\mathrm{E}\circ \left(\left(1^{st}\otimes \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ 2^{nd}\right)\right)\circ {\mathrm{E}}^{-1}\right)\right)$$