Theorem mndfo

Description: The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013) (Proof shortened by AV, 17-Aug-2026)

	Ref	Expression
Hypotheses	mndfo.b	|- B = ( Base ` G )
	mndfo.p	|- .+ = ( +g ` G )
Assertion	mndfo	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		mndfo.b	|- B = ( Base ` G )
2		mndfo.p	|- .+ = ( +g ` G )
3		mndmgm	|- ( G e. Mnd -> G e. Mgm )
4	3	adantr	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> G e. Mgm )
5	1 2	mndid	|- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
6	5	adantr	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) )
7		simpr	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ Fn ( B X. B ) )
8	1 2 4 6 7	mgmfod	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )