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 = ( 𝑔 ∈ Grp , 𝑠 ∈ { ∣ ( : dom ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ( ∀ 𝑦 ∈ ( dom ∖ { 𝑥 } ) ( 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( 𝑦 ) ) ∧ ( ( 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ( “ ( dom ∖ { 𝑥 } ) ) ) ) = { ( 0g𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { X 𝑥 ∈ dom 𝑠 ( 𝑠𝑥 ) ∣ finSupp ( 0g𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) )
2 1 reldmmpo Rel dom DProd