Definition df-fullfun 5769

Description: Define the full function operator. This is a function over _V that agrees with the function value of F at every point. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-fullfun	|- FullFun F = ((( _I o. F) \ ( ∼ _I o. F)) u. ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)}))

Detailed syntax breakdown of Definition df-fullfun

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	cfullfun 5768	. 2 class FullFun F
3		cid 4764	. . . . 5 class _I
4	3, 1	ccom 4722	. . . 4 class ( _I o. F)
5	3	ccompl 3206	. . . . 5 class ∼ _I
6	5, 1	ccom 4722	. . . 4 class ( ∼ _I o. F)
7	4, 6	cdif 3207	. . 3 class (( _I o. F) \ ( ∼ _I o. F))
8	7	cdm 4773	. . . . 5 class dom (( _I o. F) \ ( ∼ _I o. F))
9	8	ccompl 3206	. . . 4 class ∼ dom (( _I o. F) \ ( ∼ _I o. F))
10		c0 3551	. . . . 5 class (/)
11	10	csn 3738	. . . 4 class {(/)}
12	9, 11	cxp 4771	. . 3 class ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)})
13	7, 12	cun 3208	. 2 class ((( _I o. F) \ ( ∼ _I o. F)) u. ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)}))
14	2, 13	wceq 1642	1 wff FullFun F = ((( _I o. F) \ ( ∼ _I o. F)) u. ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)}))

This definition is referenced by:  fnfullfun  5859  fullfunexg  5860  fvfullfun  5865