Metamath Proof Explorer


Theorem fnfuc

Description: The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Assertion fnfuc FuncCatFnCat×Cat

Proof

Step Hyp Ref Expression
1 df-fuc FuncCat=tCat,uCatBasendxtFuncuHomndxtNatucompndxvtFuncu×tFuncu,htFuncu1stv/f2ndv/gbgtNatuh,aftNatugxBasetbx1stfx1stgxcompu1sthxax
2 tpex BasendxtFuncuHomndxtNatucompndxvtFuncu×tFuncu,htFuncu1stv/f2ndv/gbgtNatuh,aftNatugxBasetbx1stfx1stgxcompu1sthxaxV
3 1 2 fnmpoi FuncCatFnCat×Cat