Theorem mgmfod

Description: The operation of a magma with identity is an onto function (assuming it is a function). (Contributed by FL, 2-Nov-2009) (Revised by AV, 16-Aug-2026)

	Ref	Expression
Hypotheses	mgmidpfod.b	$$⊢B={\mathrm{Base}}_G$$
	mgmidpfod.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mgmidpfod.g	$$⊢\phi \to G\in \mathrm{Mgm}$$
	mgmidpfod.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
	mgmfod.f	$$⊢\phi \to \underset{\dot{}}{+}Fn\left(B\times B\right)$$
Assertion	mgmfod	$$⊢\phi \to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		mgmidpfod.b	$$⊢B={\mathrm{Base}}_G$$
2		mgmidpfod.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mgmidpfod.g	$$⊢\phi \to G\in \mathrm{Mgm}$$
4		mgmidpfod.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
5		mgmfod.f	$$⊢\phi \to \underset{\dot{}}{+}Fn\left(B\times B\right)$$
6		eqid	$$⊢{+}_{𝑓}\left(G\right)={+}_{𝑓}\left(G\right)$$
7	1 2 3 4 6	mgmidpfod	$$⊢\phi \to {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B$$
8	1 2 6	plusfeq	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to {+}_{𝑓}\left(G\right)=\underset{\dot{}}{+}$$
9	5 8	syl	$$⊢\phi \to {+}_{𝑓}\left(G\right)=\underset{\dot{}}{+}$$
10	9	eqcomd	$$⊢\phi \to \underset{\dot{}}{+}={+}_{𝑓}\left(G\right)$$
11		foeq1	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(G\right)\to \left(\underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B\leftrightarrow {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B\right)$$
12	10 11	syl	$$⊢\phi \to \left(\underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B\leftrightarrow {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B\right)$$
13	7 12	mpbird	$$⊢\phi \to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$