Metamath Proof Explorer


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 S V ¬ G dom 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 brrelex2i G dom DProd S S V
7 4 6 nsyl dom S V ¬ G dom DProd S