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 e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
2 1 reldmmpo 
 |-  Rel dom toNrmGrp