Metamath Proof Explorer

Theorem termofn

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

Ref Expression
Assertion termofn 
|- TermO 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. ( b ( Hom ` c ) a ) } e. _V
3 df-termo 
 |-  TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
4 2 3 fnmpti 
 |-  TermO Fn Cat