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	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	elxpcbasex2ALT	⊢ ( 𝜑 → 𝐷 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elxpcbasex1.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6	1 4 5	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
7	2 6	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
8	3 7	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
9		xp2nd	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
11	10	elfvexd	⊢ ( 𝜑 → 𝐷 ∈ V )