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 = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
Assertion	xpcfucbas	|- ( ( B Func C ) X. ( D Func E ) ) = ( Base ` T )

Proof

Step	Hyp	Ref	Expression
1		xpcfucbas.t	|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
2		eqid	|- ( B FuncCat C ) = ( B FuncCat C )
3	2	fucbas	|- ( B Func C ) = ( Base ` ( B FuncCat C ) )
4		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
5	4	fucbas	|- ( D Func E ) = ( Base ` ( D FuncCat E ) )
6	1 3 5	xpcbas	|- ( ( B Func C ) X. ( D Func E ) ) = ( Base ` T )