Theorem dprdval0prc

Description: The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019)

	Ref	Expression
Assertion	dprdval0prc	⊢ ( dom 𝑆 ∉ V → ( 𝐺 DProd 𝑆 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V )
2		dmexg	⊢ ( 𝑆 ∈ V → dom 𝑆 ∈ V )
3	2	con3i	⊢ ( ¬ dom 𝑆 ∈ V → ¬ 𝑆 ∈ V )
4	1 3	sylbi	⊢ ( dom 𝑆 ∉ V → ¬ 𝑆 ∈ V )
5		reldmdprd	⊢ Rel dom DProd
6	5	ovprc2	⊢ ( ¬ 𝑆 ∈ V → ( 𝐺 DProd 𝑆 ) = ∅ )
7	4 6	syl	⊢ ( dom 𝑆 ∉ V → ( 𝐺 DProd 𝑆 ) = ∅ )