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

Metamath Proof Explorer

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	$⊢ 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = {F ↾}_{dom ((𝖨𝗆𝖺𝗀𝖾 F \circ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) \cap (V \times 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))}$

Detailed syntax breakdown

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