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 F

Proof

Step Hyp Ref Expression
1 df-funpart 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
2 resss F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 F
3 1 2 eqsstri 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F F