Definition df-fullfun 5768

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 5767	. 2 class FullFun F
3		cid 4763	. . . . 5 class _I
4	3, 1	ccom 4721	. . . 4 class ( _I o. F)
5	3	ccompl 3205	. . . . 5 class ∼ _I
6	5, 1	ccom 4721	. . . 4 class ( ∼ _I o. F)
7	4, 6	cdif 3206	. . 3 class (( _I o. F) \ ( ∼ _I o. F))
8	7	cdm 4772	. . . . 5 class dom (( _I o. F) \ ( ∼ _I o. F))
9	8	ccompl 3205	. . . 4 class ∼ dom (( _I o. F) \ ( ∼ _I o. F))
10		c0 3550	. . . . 5 class (/)
11	10	csn 3737	. . . 4 class {(/)}
12	9, 11	cxp 4770	. . 3 class ( ∼ dom (( _I o. F) \ ( ∼ _I o. F)) X. {(/)})
13	7, 12	cun 3207	. 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  5858  fullfunexg  5859  fvfullfun  5864