Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-zeroo | Structured version Visualization version GIF version |
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 |
---|---|
df-zeroo | ⊢ ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | czeroo 17708 | . 2 class ZeroO | |
2 | vc | . . 3 setvar 𝑐 | |
3 | ccat 17383 | . . 3 class Cat | |
4 | 2 | cv 1538 | . . . . 5 class 𝑐 |
5 | cinito 17706 | . . . . 5 class InitO | |
6 | 4, 5 | cfv 6426 | . . . 4 class (InitO‘𝑐) |
7 | ctermo 17707 | . . . . 5 class TermO | |
8 | 4, 7 | cfv 6426 | . . . 4 class (TermO‘𝑐) |
9 | 6, 8 | cin 3885 | . . 3 class ((InitO‘𝑐) ∩ (TermO‘𝑐)) |
10 | 2, 3, 9 | cmpt 5156 | . 2 class (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐))) |
11 | 1, 10 | wceq 1539 | 1 wff ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐))) |
Colors of variables: wff setvar class |
This definition is referenced by: zeroofn 17714 zeroorcl 17717 zerooval 17720 |
Copyright terms: Public domain | W3C validator |