Theorem dprddomprc

Description: A family of subgroups indexed by a proper class cannot be a family of subgroups for an internal direct product. (Contributed by AV, 13-Jul-2019)

	Ref	Expression
Assertion	dprddomprc	$$⊢\mathrm{dom}S\notin \mathrm{V}\to \neg G\mathrm{dom}\mathrm{DProd}S$$

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	brrelex2i	$$⊢G\mathrm{dom}\mathrm{DProd}S\to S\in \mathrm{V}$$
7	4 6	nsyl	$$⊢\mathrm{dom}S\notin \mathrm{V}\to \neg G\mathrm{dom}\mathrm{DProd}S$$