Theorem grpplusfo

Description: The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	grpplusf.1	|- B = ( Base ` G )
	grpplusf.2	|- F = ( +f ` G )
Assertion	grpplusfo	|- ( G e. Grp -> F : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		grpplusf.1	|- B = ( Base ` G )
2		grpplusf.2	|- F = ( +f ` G )
3		grpmnd	|- ( G e. Grp -> G e. Mnd )
4	1 2	mndpfo	|- ( G e. Mnd -> F : ( B X. B ) -onto-> B )
5	3 4	syl	|- ( G e. Grp -> F : ( B X. B ) -onto-> B )