Theorem elxpcbasex1ALT

Description: Alternate proof of elxpcbasex1 . (Contributed by Zhi Wang, 8-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elxpcbasex1.t	|- T = ( C Xc. D )
	elxpcbasex1.b	|- B = ( Base ` T )
	elxpcbasex1.x	|- ( ph -> X e. B )
Assertion	elxpcbasex1ALT	|- ( 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		eqid	|- ( Base ` C ) = ( Base ` C )
5		eqid	|- ( Base ` D ) = ( Base ` D )
6	1 4 5	xpcbas	|- ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` T )
7	2 6	eqtr4i	|- B = ( ( Base ` C ) X. ( Base ` D ) )
8	3 7	eleqtrdi	|- ( ph -> X e. ( ( Base ` C ) X. ( Base ` D ) ) )
9		xp1st	|- ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> ( 1st ` X ) e. ( Base ` C ) )
10	8 9	syl	|- ( ph -> ( 1st ` X ) e. ( Base ` C ) )
11	10	elfvexd	|- ( ph -> C e. _V )