This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \subseteq F$

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