Metamath Proof Explorer


Theorem termofn

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

Ref Expression
Assertion termofn TermOFnCat

Proof

Step Hyp Ref Expression
1 fvex BasecV
2 1 rabex aBasec|bBasec∃!hhbHomcaV
3 df-termo TermO=cCataBasec|bBasec∃!hhbHomca
4 2 3 fnmpti TermOFnCat