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{\times }_{c}D$$
	elxpcbasex1.b	$$⊢B={\mathrm{Base}}_T$$
	elxpcbasex1.x	$$⊢\phi \to X\in B$$
Assertion	elxpcbasex1ALT	$$⊢\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		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
6	1 4 5	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_T$$
7	2 6	eqtr4i	$$⊢B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
8	3 7	eleqtrdi	$$⊢\phi \to X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
9		xp1st	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
10	8 9	syl	$$⊢\phi \to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
11	10	elfvexd	$$⊢\phi \to C\in \mathrm{V}$$