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={\mathrm{Base}}_G$$
	mndpfo.p	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	mndpfo	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		mndpfo.b	$$⊢B={\mathrm{Base}}_G$$
2		mndpfo.p	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
3		eqid	$$⊢{+}_G={+}_G$$
4		mndmgm	$$⊢G\in \mathrm{Mnd}\to G\in \mathrm{Mgm}$$
5	1 3	mndid	$$⊢G\in \mathrm{Mnd}\to \exists i\in B\forall x\in B\left(i{+}_{G}x=x\wedge x{+}_{G}i=x\right)$$
6	1 3 4 5 2	mgmidpfod	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B$$