This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldmdprd

Description: The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016) (Proof shortened by AV, 11-Jul-2019)

Ref Expression
Assertion reldmdprd ⊢ Rel ⁡ dom ⁡ DProd

Proof

Step Hyp Ref Expression
1 df-dprd ⊢ DProd = g ∈ Grp , s ∈ h | h : dom ⁡ h ⟶ SubGrp ⁡ g ∧ ∀ x ∈ dom ⁡ h ∀ y ∈ dom ⁡ h ∖ x h ⁡ x ⊆ Cntz ⁡ g ⁡ h ⁡ y ∧ h ⁡ x ∩ mrCls ⁡ SubGrp ⁡ g ⁡ ⋃ h dom ⁡ h ∖ x = 0 g ⟼ ran ⁡ f ∈ h ∈ ⨉ x ∈ dom ⁡ s s ⁡ x | finSupp 0 g⁡ h ⟼ ∑ g f
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ DProd