Theorem elxpcbasex1

Description: A non-empty base set of the product category indicates the existence of the first factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025) (Proof shortened by SN, 15-Oct-2025)

	Ref	Expression
Hypotheses	elxpcbasex1.t	$$⊢T=C{\times }_{c}D$$
	elxpcbasex1.b	$$⊢B={\mathrm{Base}}_T$$
	elxpcbasex1.x	$$⊢\phi \to X\in B$$
Assertion	elxpcbasex1	$$⊢\phi \to C\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		elxpcbasex1.t	$$⊢T=C{\times }_{c}D$$
2		elxpcbasex1.b	$$⊢B={\mathrm{Base}}_T$$
3		elxpcbasex1.x	$$⊢\phi \to X\in B$$
4		reldmxpc	$$⊢\mathrm{Rel}\mathrm{dom}{\times }_c$$
5	1 2 4	strov2rcl	$$⊢X\in B\to C\in \mathrm{V}$$
6	3 5	syl	$$⊢\phi \to C\in \mathrm{V}$$