Metamath Proof Explorer

Theorem oppcinito

Description: Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025)

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

Proof

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