Theorem elxpcbasex2ALT

Description: Alternate proof of elxpcbasex2 . (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	elxpcbasex2ALT	$$⊢\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		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		xp2nd	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
10	8 9	syl	$$⊢\phi \to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
11	10	elfvexd	$$⊢\phi \to D\in \mathrm{V}$$