Theorem elxpcbasex2

Description: A non-empty base set of the product category indicates the existence of the second factor of the product category. (Contributed by Zhi Wang, 8-Oct-2025) (Proof shortened by SN, 15-Oct-2025)

	Ref	Expression
Hypotheses	elxpcbasex1.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	elxpcbasex2	⊢ ( 𝜑 → 𝐷 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elxpcbasex1.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		elxpcbasex1.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		elxpcbasex1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		reldmxpc	⊢ Rel dom ×c
5	4 1 2	elbasov	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
7	6	simprd	⊢ ( 𝜑 → 𝐷 ∈ V )