Theorem funpartss

Description: The functional part of F is a subset of F . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	funpartss	$$⊢\mathrm{𝖥𝗎𝗇𝖯𝖺𝗋𝗍}F\subseteq F$$

Proof

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