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	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
	dprddomcld.2	$$⊢\phi \to \mathrm{dom}S=I$$
Assertion	dprddomcld	$$⊢\phi \to I\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		dprddomcld.1	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}S$$
2		dprddomcld.2	$$⊢\phi \to \mathrm{dom}S=I$$
3		df-nel	$$⊢\mathrm{dom}S\notin \mathrm{V}\leftrightarrow \neg \mathrm{dom}S\in \mathrm{V}$$
4		dprddomprc	$$⊢\mathrm{dom}S\notin \mathrm{V}\to \neg G\mathrm{dom}\mathrm{DProd}S$$
5	3 4	sylbir	$$⊢\neg \mathrm{dom}S\in \mathrm{V}\to \neg G\mathrm{dom}\mathrm{DProd}S$$
6	5	con4i	$$⊢G\mathrm{dom}\mathrm{DProd}S\to \mathrm{dom}S\in \mathrm{V}$$
7		eleq1	$$⊢\mathrm{dom}S=I\to \left(\mathrm{dom}S\in \mathrm{V}\leftrightarrow I\in \mathrm{V}\right)$$
8	6 7	imbitrid	$$⊢\mathrm{dom}S=I\to \left(G\mathrm{dom}\mathrm{DProd}S\to I\in \mathrm{V}\right)$$
9	2 1 8	sylc	$$⊢\phi \to I\in \mathrm{V}$$