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)) × {∅})) |