Metamath Proof Explorer


Theorem reldmtng

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

Ref Expression
Assertion reldmtng Rel dom toNrmGrp

Proof

Step Hyp Ref Expression
1 df-tng toNrmGrp = g V , f V g sSet dist ndx f - g sSet TopSet ndx MetOpen f - g
2 1 reldmmpo Rel dom toNrmGrp