Theorem dprddomcld

Description: If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019)

	Ref	Expression
Hypotheses	dprddomcld.1	|- ( ph -> G dom DProd S )
	dprddomcld.2	|- ( ph -> dom S = I )
Assertion	dprddomcld	|- ( ph -> I e. _V )

Proof

Step	Hyp	Ref	Expression
1		dprddomcld.1	|- ( ph -> G dom DProd S )
2		dprddomcld.2	|- ( ph -> dom S = I )
3		df-nel	|- ( dom S e/ _V <-> -. dom S e. _V )
4		dprddomprc	|- ( dom S e/ _V -> -. G dom DProd S )
5	3 4	sylbir	|- ( -. dom S e. _V -> -. G dom DProd S )
6	5	con4i	|- ( G dom DProd S -> dom S e. _V )
7		eleq1	|- ( dom S = I -> ( dom S e. _V <-> I e. _V ) )
8	6 7	imbitrid	|- ( dom S = I -> ( G dom DProd S -> I e. _V ) )
9	2 1 8	sylc	|- ( ph -> I e. _V )