This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( ZeroO ` C ) <-> I e. ( ZeroO ` ( oppCat ` C ) ) )

Proof

Step Hyp Ref Expression
1 zeroorcl 
 |-  ( I e. ( ZeroO ` C ) -> C e. Cat )
2 zeroorcl 
 |-  ( I e. ( ZeroO ` ( oppCat ` C ) ) -> ( oppCat ` C ) e. 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 e. ( ZeroO ` ( oppCat ` C ) ) -> I e. ( Base ` C ) )
7 elfvex 
 |-  ( I e. ( Base ` C ) -> C e. _V )
8 id 
 |-  ( C e. _V -> C e. _V )
9 3 8 oppccatb 
 |-  ( C e. _V -> ( C e. Cat <-> ( oppCat ` C ) e. Cat ) )
10 6 7 9 3syl 
 |-  ( I e. ( ZeroO ` ( oppCat ` C ) ) -> ( C e. Cat <-> ( oppCat ` C ) e. Cat ) )
11 2 10 mpbird 
 |-  ( I e. ( ZeroO ` ( oppCat ` C ) ) -> C e. Cat )
12 oppcinito 
 |-  ( c e. ( InitO ` C ) <-> c e. ( TermO ` ( oppCat ` C ) ) )
13 12 eqriv 
 |-  ( InitO ` C ) = ( TermO ` ( oppCat ` C ) )
14 oppctermo 
 |-  ( c e. ( TermO ` C ) <-> c e. ( InitO ` ( oppCat ` C ) ) )
15 14 eqriv 
 |-  ( TermO ` C ) = ( InitO ` ( oppCat ` C ) )
16 13 15 ineq12i 
 |-  ( ( InitO ` C ) i^i ( TermO ` C ) ) = ( ( TermO ` ( oppCat ` C ) ) i^i ( InitO ` ( oppCat ` C ) ) )
17 incom 
 |-  ( ( TermO ` ( oppCat ` C ) ) i^i ( InitO ` ( oppCat ` C ) ) ) = ( ( InitO ` ( oppCat ` C ) ) i^i ( TermO ` ( oppCat ` C ) ) )
18 16 17 eqtri 
 |-  ( ( InitO ` C ) i^i ( TermO ` C ) ) = ( ( InitO ` ( oppCat ` C ) ) i^i ( TermO ` ( oppCat ` C ) ) )
19 id 
 |-  ( C e. Cat -> C e. Cat )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 19 4 20 zerooval 
 |-  ( C e. Cat -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )
22 3 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
23 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
24 22 5 23 zerooval 
 |-  ( C e. Cat -> ( ZeroO ` ( oppCat ` C ) ) = ( ( InitO ` ( oppCat ` C ) ) i^i ( TermO ` ( oppCat ` C ) ) ) )
25 18 21 24 3eqtr4a 
 |-  ( C e. Cat -> ( ZeroO ` C ) = ( ZeroO ` ( oppCat ` C ) ) )
26 25 eleq2d 
 |-  ( C e. Cat -> ( I e. ( ZeroO ` C ) <-> I e. ( ZeroO ` ( oppCat ` C ) ) ) )
27 1 11 26 pm5.21nii 
 |-  ( I e. ( ZeroO ` C ) <-> I e. ( ZeroO ` ( oppCat ` C ) ) )