Theorem xpcfucbas

Description: The base set of the product of two categories of functors. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypothesis	xpcfucbas.t	$$⊢T=\left(B\mathrm{FuncCat}C\right){\times }_c\left(D\mathrm{FuncCat}E\right)$$
Assertion	xpcfucbas	$$⊢\left(B\mathrm{Func}C\right)\times \left(D\mathrm{Func}E\right)={\mathrm{Base}}_T$$

Proof

Step	Hyp	Ref	Expression
1		xpcfucbas.t	$$⊢T=\left(B\mathrm{FuncCat}C\right){\times }_c\left(D\mathrm{FuncCat}E\right)$$
2		eqid	$$⊢B\mathrm{FuncCat}C=B\mathrm{FuncCat}C$$
3	2	fucbas	$$⊢B\mathrm{Func}C={\mathrm{Base}}_{\left(B\mathrm{FuncCat}C\right)}$$
4		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
5	4	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_{\left(D\mathrm{FuncCat}E\right)}$$
6	1 3 5	xpcbas	$$⊢\left(B\mathrm{Func}C\right)\times \left(D\mathrm{Func}E\right)={\mathrm{Base}}_T$$