# Metamath Proof Explorer

## Theorem fnxpc

Description: The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Assertion fnxpc ${⊢}{×}_{c}Fn\left(\mathrm{V}×\mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 df-xpc
2 tpex ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({x}\in \left({b}×{b}\right),{y}\in {b}⟼\left({g}\in \left({2}^{nd}\left({x}\right){h}{y}\right),{f}\in {h}\left({x}\right)⟼⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩\right)\right)⟩\right\}\in \mathrm{V}$
3 2 csbex
4 3 csbex
5 1 4 fnmpoi ${⊢}{×}_{c}Fn\left(\mathrm{V}×\mathrm{V}\right)$