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