Description: The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isinito.b | ⊢ 𝐵 = ( Base ‘ 𝐶 ) | |
isinito.h | ⊢ 𝐻 = ( Hom ‘ 𝐶 ) | ||
isinito.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | ||
isinito.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 ) | ||
Assertion | iszeroo | ⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isinito.b | ⊢ 𝐵 = ( Base ‘ 𝐶 ) | |
2 | isinito.h | ⊢ 𝐻 = ( Hom ‘ 𝐶 ) | |
3 | isinito.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | |
4 | isinito.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 ) | |
5 | 3 1 2 | zerooval | ⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ) |
6 | 5 | eleq2d | ⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ 𝐼 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ) ) |
7 | elin | ⊢ ( 𝐼 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) ) | |
8 | 6 7 | bitrdi | ⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) ) ) |