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 ×cFnV×V

Proof

Step Hyp Ref Expression
1 df-xpc ×c=rV,sVBaser×Bases/bub,vb1stuHomr1stv×2nduHoms2ndv/hBasendxbHomndxhcompndxxb×b,ybg2ndxhy,fhx1stg1st1stx1st2ndxcompr1sty1stf2ndg2nd1stx2nd2ndxcomps2ndy2ndf
2 tpex BasendxbHomndxhcompndxxb×b,ybg2ndxhy,fhx1stg1st1stx1st2ndxcompr1sty1stf2ndg2nd1stx2nd2ndxcomps2ndy2ndfV
3 2 csbex ub,vb1stuHomr1stv×2nduHoms2ndv/hBasendxbHomndxhcompndxxb×b,ybg2ndxhy,fhx1stg1st1stx1st2ndxcompr1sty1stf2ndg2nd1stx2nd2ndxcomps2ndy2ndfV
4 3 csbex Baser×Bases/bub,vb1stuHomr1stv×2nduHoms2ndv/hBasendxbHomndxhcompndxxb×b,ybg2ndxhy,fhx1stg1st1stx1st2ndxcompr1sty1stf2ndg2nd1stx2nd2ndxcomps2ndy2ndfV
5 1 4 fnmpoi ×cFnV×V