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 = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑔 sSet ⟨ ( dist ‘ ndx ) , ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ⟩ ) sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( 𝑓 ∘ ( -g ‘ 𝑔 ) ) ) ⟩ ) )
2	1	reldmmpo	⊢ Rel dom toNrmGrp