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	|- ( dom S e/ _V -> -. G dom DProd S )

Proof

Step	Hyp	Ref	Expression
1		df-nel	|- ( dom S e/ _V <-> -. dom S e. _V )
2		dmexg	|- ( S e. _V -> dom S e. _V )
3	2	con3i	|- ( -. dom S e. _V -> -. S e. _V )
4	1 3	sylbi	|- ( dom S e/ _V -> -. S e. _V )
5		reldmdprd	|- Rel dom DProd
6	5	brrelex2i	|- ( G dom DProd S -> S e. _V )
7	4 6	nsyl	|- ( dom S e/ _V -> -. G dom DProd S )