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 𝑆 ∉ V → ( 𝐺 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 ovprc2 ( ¬ 𝑆 ∈ V → ( 𝐺 DProd 𝑆 ) = ∅ )
7 4 6 syl ( dom 𝑆 ∉ V → ( 𝐺 DProd 𝑆 ) = ∅ )