Metamath Proof Explorer

Theorem initofn

Description: InitO is a function on Cat . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion initofn 
|- InitO Fn Cat

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Base ` c ) e. _V
2 1 rabex 
 |-  { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } e. _V
3 df-inito 
 |-  InitO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
4 2 3 fnmpti 
 |-  InitO Fn Cat