Metamath Proof Explorer

Theorem oppczeroo

Description: Zero objects are zero in the opposite category. Remark 7.8 of Adamek p. 103. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion oppczeroo ⊢ I ∈ ZeroO ⁡ C ↔ I ∈ ZeroO ⁡ oppCat ⁡ C

Proof

Step Hyp Ref Expression
1 zeroorcl ⊢ I ∈ ZeroO ⁡ C → C ∈ Cat
2 zeroorcl ⊢ I ∈ ZeroO ⁡ oppCat ⁡ C → oppCat ⁡ C ∈ Cat
3 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
4 eqid ⊢ Base C = Base C
5 3 4 oppcbas ⊢ Base C = Base oppCat ⁡ C
6 5 zeroo2 ⊢ I ∈ ZeroO ⁡ oppCat ⁡ C → I ∈ Base C
7 elfvex ⊢ I ∈ Base C → C ∈ V
8 id ⊢ C ∈ V → C ∈ V
9 3 8 oppccatb ⊢ C ∈ V → C ∈ Cat ↔ oppCat ⁡ C ∈ Cat
10 6 7 9 3syl ⊢ I ∈ ZeroO ⁡ oppCat ⁡ C → C ∈ Cat ↔ oppCat ⁡ C ∈ Cat
11 2 10 mpbird ⊢ I ∈ ZeroO ⁡ oppCat ⁡ C → C ∈ Cat
12 oppcinito ⊢ c ∈ InitO ⁡ C ↔ c ∈ TermO ⁡ oppCat ⁡ C
13 12 eqriv ⊢ InitO ⁡ C = TermO ⁡ oppCat ⁡ C
14 oppctermo ⊢ c ∈ TermO ⁡ C ↔ c ∈ InitO ⁡ oppCat ⁡ C
15 14 eqriv ⊢ TermO ⁡ C = InitO ⁡ oppCat ⁡ C
16 13 15 ineq12i ⊢ InitO ⁡ C ∩ TermO ⁡ C = TermO ⁡ oppCat ⁡ C ∩ InitO ⁡ oppCat ⁡ C
17 incom ⊢ TermO ⁡ oppCat ⁡ C ∩ InitO ⁡ oppCat ⁡ C = InitO ⁡ oppCat ⁡ C ∩ TermO ⁡ oppCat ⁡ C
18 16 17 eqtri ⊢ InitO ⁡ C ∩ TermO ⁡ C = InitO ⁡ oppCat ⁡ C ∩ TermO ⁡ oppCat ⁡ C
19 id ⊢ C ∈ Cat → C ∈ Cat
20 eqid ⊢ Hom ⁡ C = Hom ⁡ C
21 19 4 20 zerooval ⊢ C ∈ Cat → ZeroO ⁡ C = InitO ⁡ C ∩ TermO ⁡ C
22 3 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
23 eqid ⊢ Hom ⁡ oppCat ⁡ C = Hom ⁡ oppCat ⁡ C
24 22 5 23 zerooval ⊢ C ∈ Cat → ZeroO ⁡ oppCat ⁡ C = InitO ⁡ oppCat ⁡ C ∩ TermO ⁡ oppCat ⁡ C
25 18 21 24 3eqtr4a ⊢ C ∈ Cat → ZeroO ⁡ C = ZeroO ⁡ oppCat ⁡ C
26 25 eleq2d ⊢ C ∈ Cat → I ∈ ZeroO ⁡ C ↔ I ∈ ZeroO ⁡ oppCat ⁡ C
27 1 11 26 pm5.21nii ⊢ I ∈ ZeroO ⁡ C ↔ I ∈ ZeroO ⁡ oppCat ⁡ C