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 ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ 𝐼 ∈ ( ZeroO ‘ ( oppCat ‘ 𝐶 ) ) )

Proof

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