Definition df-funpart

Description: Define the functional part of a class F . This is the maximal part of F that is a function. See funpartfun and funpartfv for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014)

	Ref	Expression
Assertion	df-funpart	$$⊢\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F={F\upharpoonright }_{\mathrm{dom}\left(\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\cap \left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)\right)}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	cfunpart	$$class\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F$$
2	0	cimage	$$class\mathrm{𝖨𝗆𝖺𝗀𝖾}F$$
3		csingle	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}$$
4	2 3	ccom	$$class\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)$$
5		cvv	$$class\mathrm{V}$$
6		csingles	$$class\mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}$$
7	5 6	cxp	$$class\left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)$$
8	4 7	cin	$$class\left(\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\cap \left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)\right)$$
9	8	cdm	$$class\mathrm{dom}\left(\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\cap \left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)\right)$$
10	0 9	cres	$$class\left({F\upharpoonright }_{\mathrm{dom}\left(\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\cap \left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)\right)}\right)$$
11	1 10	wceq	$$wff\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F={F\upharpoonright }_{\mathrm{dom}\left(\left(\mathrm{𝖨𝗆𝖺𝗀𝖾}F\circ \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇}\right)\cap \left(\mathrm{V}\times \mathrm{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}\right)\right)}$$