Theorem elxpcbasex2

Description: A non-empty base set of the product category indicates the existence of the second 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	elxpcbasex2	$$⊢\phi \to D\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	4 1 2	elbasov	$$⊢X\in B\to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
6	3 5	syl	$$⊢\phi \to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
7	6	simprd	$$⊢\phi \to D\in \mathrm{V}$$