Metamath Proof Explorer

Theorem initoval

Description: The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses initoval.c 
|- ( ph -> C e. Cat )
initoval.b 
|- B = ( Base ` C )
initoval.h 
|- H = ( Hom ` C )
Assertion initoval 
|- ( ph -> ( InitO ` C ) = { a e. B | A. b e. B E! h h e. ( a H b ) } )

Proof

Step Hyp Ref Expression
1 initoval.c 
 |-  ( ph -> C e. Cat )
2 initoval.b 
 |-  B = ( Base ` C )
3 initoval.h 
 |-  H = ( Hom ` C )
4 df-inito 
 |-  InitO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
5 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
6 5 2 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
7 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
8 7 3 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
9 8 oveqd 
 |-  ( c = C -> ( a ( Hom ` c ) b ) = ( a H b ) )
10 9 eleq2d 
 |-  ( c = C -> ( h e. ( a ( Hom ` c ) b ) <-> h e. ( a H b ) ) )
11 10 eubidv 
 |-  ( c = C -> ( E! h h e. ( a ( Hom ` c ) b ) <-> E! h h e. ( a H b ) ) )
12 6 11 raleqbidv 
 |-  ( c = C -> ( A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) <-> A. b e. B E! h h e. ( a H b ) ) )
13 6 12 rabeqbidv 
 |-  ( c = C -> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } = { a e. B | A. b e. B E! h h e. ( a H b ) } )
14 2 fvexi 
 |-  B e. _V
15 14 rabex 
 |-  { a e. B | A. b e. B E! h h e. ( a H b ) } e. _V
16 15 a1i 
 |-  ( ph -> { a e. B | A. b e. B E! h h e. ( a H b ) } e. _V )
17 4 13 1 16 fvmptd3 
 |-  ( ph -> ( InitO ` C ) = { a e. B | A. b e. B E! h h e. ( a H b ) } )