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 e/ _V -> -. G dom DProd S )

Proof

Step Hyp Ref Expression
1 df-nel
 |-  ( dom S e/ _V <-> -. dom S e. _V )
2 dmexg
 |-  ( S e. _V -> dom S e. _V )
3 2 con3i
 |-  ( -. dom S e. _V -> -. S e. _V )
4 1 3 sylbi
 |-  ( dom S e/ _V -> -. S e. _V )
5 reldmdprd
 |-  Rel dom DProd
6 5 brrelex2i
 |-  ( G dom DProd S -> S e. _V )
7 4 6 nsyl
 |-  ( dom S e/ _V -> -. G dom DProd S )