Metamath Proof Explorer

Theorem dftermo2

Description: A terminal object is an initial object in the opposite category. An alternate definition of df-termo depending on df-inito . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo2 
|- TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )

Proof

Step Hyp Ref Expression
1 df-termo 
 |-  TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
2 eqid 
 |-  ( oppCat ` c ) = ( oppCat ` c )
3 2 oppccat 
 |-  ( c e. Cat -> ( oppCat ` c ) e. Cat )
4 eqid 
 |-  ( Base ` c ) = ( Base ` c )
5 2 4 oppcbas 
 |-  ( Base ` c ) = ( Base ` ( oppCat ` c ) )
6 eqid 
 |-  ( Hom ` ( oppCat ` c ) ) = ( Hom ` ( oppCat ` c ) )
7 3 5 6 initoval 
 |-  ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` ( oppCat ` c ) ) b ) } )
8 eqid 
 |-  ( Hom ` c ) = ( Hom ` c )
9 8 2 oppchom 
 |-  ( a ( Hom ` ( oppCat ` c ) ) b ) = ( b ( Hom ` c ) a )
10 9 eleq2i 
 |-  ( h e. ( a ( Hom ` ( oppCat ` c ) ) b ) <-> h e. ( b ( Hom ` c ) a ) )
11 10 eubii 
 |-  ( E! h h e. ( a ( Hom ` ( oppCat ` c ) ) b ) <-> E! h h e. ( b ( Hom ` c ) a ) )
12 11 ralbii 
 |-  ( A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` ( oppCat ` c ) ) b ) <-> A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) )
13 12 rabbii 
 |-  { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` ( oppCat ` c ) ) b ) } = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) }
14 7 13 eqtrdi 
 |-  ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
15 14 mpteq2ia 
 |-  ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
16 1 15 eqtr4i 
 |-  TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )