Metamath Proof Explorer


Theorem fnmgp

Description: The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Assertion fnmgp mulGrp Fn V

Proof

Step Hyp Ref Expression
1 ovex ( 𝑥 sSet ⟨ ( +g ‘ ndx ) , ( .r𝑥 ) ⟩ ) ∈ V
2 df-mgp mulGrp = ( 𝑥 ∈ V ↦ ( 𝑥 sSet ⟨ ( +g ‘ ndx ) , ( .r𝑥 ) ⟩ ) )
3 1 2 fnmpti mulGrp Fn V