Metamath Proof Explorer

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

Proof

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