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

Metamath Proof Explorer

Definition df-fullfun

Description: Define the full function over F . This is a function with domain _V that always agrees with F for its value. (Contributed by Scott Fenton, 17-Apr-2014)

		Ref	Expression
	Assertion	df-fullfun	$⊢ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$class F$
1	0	cfullfn	$class 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F$
2	0	cfunpart	$class 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
3		cvv	$class V$
4	2	cdm	$class dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F$
5	3 4	cdif	$class (V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F)$
6		c0	$class \emptyset$
7	6	csn	$class \{\emptyset\}$
8	5 7	cxp	$class ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})$
9	2 8	cun	$class (𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\}))$
10	1 9	wceq	$wff 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F \cup ((V ∖ dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F) \times \{\emptyset\})$