Metamath Proof Explorer


Theorem dprdval0prc

Description: The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019)

Ref Expression
Assertion dprdval0prc dom S V G DProd S =

Proof

Step Hyp Ref Expression
1 df-nel dom S V ¬ dom S V
2 dmexg S V dom S V
3 2 con3i ¬ dom S V ¬ S V
4 1 3 sylbi dom S V ¬ S V
5 reldmdprd Rel dom DProd
6 5 ovprc2 ¬ S V G DProd S =
7 4 6 syl dom S V G DProd S =