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	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{DProd}$$

Proof

Step	Hyp	Ref	Expression
1		df-dprd	$$⊢\mathrm{DProd}=\left(g\in \mathrm{Grp},s\in \left\{h|\left(h:\mathrm{dom}h⟶\mathrm{SubGrp}\left(g\right)\wedge \forall x\in \mathrm{dom}h\left(\forall y\in \left(\mathrm{dom}h\setminus \left\{x\right\}\right)h\left(x\right)\subseteq \mathrm{Cntz}\left(g\right)\left(h\left(y\right)\right)\wedge h\left(x\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left(g\right)\right)\left(\bigcup h\left[\mathrm{dom}h\setminus \left\{x\right\}\right]\right)=\left\{0_g\right\}\right)\right)\right\}⟼\mathrm{ran}\left(f\in \left\{h\in \underset{x\in \mathrm{dom}s}{⨉}s\left(x\right)|{finSupp}_{0_g}\left(h\right)\right\}⟼{\sum }_{g}f\right)\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{DProd}$$