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	$$⊢\mathrm{dom}S\notin \mathrm{V}\to G\mathrm{DProd}S=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢\mathrm{dom}S\notin \mathrm{V}\leftrightarrow \neg \mathrm{dom}S\in \mathrm{V}$$
2		dmexg	$$⊢S\in \mathrm{V}\to \mathrm{dom}S\in \mathrm{V}$$
3	2	con3i	$$⊢\neg \mathrm{dom}S\in \mathrm{V}\to \neg S\in \mathrm{V}$$
4	1 3	sylbi	$$⊢\mathrm{dom}S\notin \mathrm{V}\to \neg S\in \mathrm{V}$$
5		reldmdprd	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{DProd}$$
6	5	ovprc2	$$⊢\neg S\in \mathrm{V}\to G\mathrm{DProd}S=\varnothing$$
7	4 6	syl	$$⊢\mathrm{dom}S\notin \mathrm{V}\to G\mathrm{DProd}S=\varnothing$$