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 
 |-  ( x sSet <. ( +g ` ndx ) , ( .r ` x ) >. ) e. _V
2 df-mgp 
 |-  mulGrp = ( x e. _V |-> ( x sSet <. ( +g ` ndx ) , ( .r ` x ) >. ) )
3 1 2 fnmpti 
 |-  mulGrp Fn _V