Theorem fnxpc

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

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

Proof

Step	Hyp	Ref	Expression
1		df-xpc	$$⊢{\times }_c=\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\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\}\right)$$
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\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\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	$$⊢⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\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}$$
4	3	csbex	$$⊢⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\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}$$
5	1 4	fnmpoi	$$⊢{\times }_{c}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$