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 ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))

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 ∘ F)
5	3	ccompl 3206	. . . . 5 class ∼ I
6	5, 1	ccom 4722	. . . 4 class ( ∼ I ∘ F)
7	4, 6	cdif 3207	. . 3 class (( I ∘ F) ∖ ( ∼ I ∘ F))
8	7	cdm 4773	. . . . 5 class dom (( I ∘ F) ∖ ( ∼ I ∘ F))
9	8	ccompl 3206	. . . 4 class ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F))
10		c0 3551	. . . . 5 class ∅
11	10	csn 3738	. . . 4 class {∅}
12	9, 11	cxp 4771	. . 3 class ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅})
13	7, 12	cun 3208	. 2 class ((( I ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))
14	2, 13	wceq 1642	1 wff FullFun F = ((( I ∘ F) ∖ ( ∼ I ∘ F)) ∪ ( ∼ dom (( I ∘ F) ∖ ( ∼ I ∘ F)) × {∅}))

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