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	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dprddomcld.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
Assertion	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		dprddomcld.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dprddomcld.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		df-nel	⊢ ( dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V )
4		dprddomprc	⊢ ( dom 𝑆 ∉ V → ¬ 𝐺 dom DProd 𝑆 )
5	3 4	sylbir	⊢ ( ¬ dom 𝑆 ∈ V → ¬ 𝐺 dom DProd 𝑆 )
6	5	con4i	⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
7		eleq1	⊢ ( dom 𝑆 = 𝐼 → ( dom 𝑆 ∈ V ↔ 𝐼 ∈ V ) )
8	6 7	imbitrid	⊢ ( dom 𝑆 = 𝐼 → ( 𝐺 dom DProd 𝑆 → 𝐼 ∈ V ) )
9	2 1 8	sylc	⊢ ( 𝜑 → 𝐼 ∈ V )