Metamath Proof Explorer

Theorem dfinito2

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

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

Proof

Step Hyp Ref Expression
1 df-inito 
 |-  InitO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
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 termoval 
 |-  ( c e. Cat -> ( TermO ` ( oppCat ` c ) ) = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` ( oppCat ` c ) ) a ) } )
8 eqid 
 |-  ( Hom ` c ) = ( Hom ` c )
9 8 2 oppchom 
 |-  ( b ( Hom ` ( oppCat ` c ) ) a ) = ( a ( Hom ` c ) b )
10 9 eleq2i 
 |-  ( h e. ( b ( Hom ` ( oppCat ` c ) ) a ) <-> h e. ( a ( Hom ` c ) b ) )
11 10 eubii 
 |-  ( E! h h e. ( b ( Hom ` ( oppCat ` c ) ) a ) <-> E! h h e. ( a ( Hom ` c ) b ) )
12 11 ralbii 
 |-  ( A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` ( oppCat ` c ) ) a ) <-> A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) )
13 12 rabbii 
 |-  { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` ( oppCat ` c ) ) a ) } = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) }
14 7 13 eqtrdi 
 |-  ( c e. Cat -> ( TermO ` ( oppCat ` c ) ) = { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
15 14 mpteq2ia 
 |-  ( c e. Cat |-> ( TermO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
16 1 15 eqtr4i 
 |-  InitO = ( c e. Cat |-> ( TermO ` ( oppCat ` c ) ) )