Theorem reldmtng

Description: The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Assertion	reldmtng	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$

Proof

Step	Hyp	Ref	Expression
1		df-tng	$$⊢\mathrm{toNrmGrp}=\left(g\in \mathrm{V},f\in \mathrm{V}⟼\left(g\mathrm{sSet}⟨\mathrm{dist}\left(\mathrm{ndx}\right),f\circ {-}_g⟩\right)\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(f\circ {-}_g\right)⟩\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{toNrmGrp}$$