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 Xc. D )
	elxpcbasex1.b	|- B = ( Base ` T )
	elxpcbasex1.x	|- ( ph -> X e. B )
Assertion	elxpcbasex1	|- ( ph -> C e. _V )

Proof

Step	Hyp	Ref	Expression
1		elxpcbasex1.t	|- T = ( C Xc. D )
2		elxpcbasex1.b	|- B = ( Base ` T )
3		elxpcbasex1.x	|- ( ph -> X e. B )
4		reldmxpc	|- Rel dom Xc.
5	1 2 4	strov2rcl	|- ( X e. B -> C e. _V )
6	3 5	syl	|- ( ph -> C e. _V )