Metamath Proof Explorer

Theorem oppctermo

Description: Terminal objects are initial in the opposite category. Comments before Definition 7.4 in Adamek p. 102. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Assertion oppctermo 
|- ( I e. ( TermO ` C ) <-> I e. ( InitO ` ( oppCat ` C ) ) )

Proof

Step Hyp Ref Expression
1 termorcl 
 |-  ( I e. ( TermO ` C ) -> C e. Cat )
2 initorcl 
 |-  ( I e. ( InitO ` ( 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 initoo2 
 |-  ( I e. ( InitO ` ( 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. ( InitO ` ( oppCat ` C ) ) -> ( C e. Cat <-> ( oppCat ` C ) e. Cat ) )
11 2 10 mpbird 
 |-  ( I e. ( InitO ` ( oppCat ` C ) ) -> C e. Cat )
12 2fveq3 
 |-  ( c = C -> ( InitO ` ( oppCat ` c ) ) = ( InitO ` ( oppCat ` C ) ) )
13 dftermo2 
 |-  TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )
14 fvex 
 |-  ( InitO ` ( oppCat ` C ) ) e. _V
15 12 13 14 fvmpt 
 |-  ( C e. Cat -> ( TermO ` C ) = ( InitO ` ( oppCat ` C ) ) )
16 15 eleq2d 
 |-  ( C e. Cat -> ( I e. ( TermO ` C ) <-> I e. ( InitO ` ( oppCat ` C ) ) ) )
17 1 11 16 pm5.21nii 
 |-  ( I e. ( TermO ` C ) <-> I e. ( InitO ` ( oppCat ` C ) ) )