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