Theorem mndpfo

Description: The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 11-Oct-2013) (Revised by AV, 23-Jan-2020) (Proof shortened by AV, 17-Aug-2026)

	Ref	Expression
Hypotheses	mndpfo.b	|- B = ( Base ` G )
	mndpfo.p	|- .+^ = ( +f ` G )
Assertion	mndpfo	|- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		mndpfo.b	|- B = ( Base ` G )
2		mndpfo.p	|- .+^ = ( +f ` G )
3		eqid	|- ( +g ` G ) = ( +g ` G )
4		mndmgm	|- ( G e. Mnd -> G e. Mgm )
5	1 3	mndid	|- ( G e. Mnd -> E. i e. B A. x e. B ( ( i ( +g ` G ) x ) = x /\ ( x ( +g ` G ) i ) = x ) )
6	1 3 4 5 2	mgmidpfod	|- ( G e. Mnd -> .+^ : ( B X. B ) -onto-> B )