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	⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1	0	cfullfn	⊢ FullFun 𝐹
2	0	cfunpart	⊢ Funpart 𝐹
3		cvv	⊢ V
4	2	cdm	⊢ dom Funpart 𝐹
5	3 4	cdif	⊢ ( V ∖ dom Funpart 𝐹 )
6		c0	⊢ ∅
7	6	csn	⊢ { ∅ }
8	5 7	cxp	⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } )
9	2 8	cun	⊢ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
10	1 9	wceq	⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )