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 𝑆 ∉ V → ¬ 𝐺 dom DProd 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V )
2		dmexg	⊢ ( 𝑆 ∈ V → dom 𝑆 ∈ V )
3	2	con3i	⊢ ( ¬ dom 𝑆 ∈ V → ¬ 𝑆 ∈ V )
4	1 3	sylbi	⊢ ( dom 𝑆 ∉ V → ¬ 𝑆 ∈ V )
5		reldmdprd	⊢ Rel dom DProd
6	5	brrelex2i	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
7	4 6	nsyl	⊢ ( dom 𝑆 ∉ V → ¬ 𝐺 dom DProd 𝑆 )