This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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