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	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
Assertion	xpcfucbas	⊢ ( ( 𝐵 Func 𝐶 ) × ( 𝐷 Func 𝐸 ) ) = ( Base ‘ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		xpcfucbas.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
2		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
3	2	fucbas	⊢ ( 𝐵 Func 𝐶 ) = ( Base ‘ ( 𝐵 FuncCat 𝐶 ) )
4		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
5	4	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
6	1 3 5	xpcbas	⊢ ( ( 𝐵 Func 𝐶 ) × ( 𝐷 Func 𝐸 ) ) = ( Base ‘ 𝑇 )