Description: An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of Adamek p. 103. (Contributed by AV, 3-Apr-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-zeroo | |- ZeroO = ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | czeroo | |- ZeroO |
|
| 1 | vc | |- c |
|
| 2 | ccat | |- Cat |
|
| 3 | cinito | |- InitO |
|
| 4 | 1 | cv | |- c |
| 5 | 4 3 | cfv | |- ( InitO ` c ) |
| 6 | ctermo | |- TermO |
|
| 7 | 4 6 | cfv | |- ( TermO ` c ) |
| 8 | 5 7 | cin | |- ( ( InitO ` c ) i^i ( TermO ` c ) ) |
| 9 | 1 2 8 | cmpt | |- ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) ) |
| 10 | 0 9 | wceq | |- ZeroO = ( c e. Cat |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) ) |