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 e/ _V -> ( G 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 ovprc2 
 |-  ( -. S e. _V -> ( G DProd S ) = (/) )
7 4 6 syl 
 |-  ( dom S e/ _V -> ( G DProd S ) = (/) )