Theorem mgmidprnd

Description: Range of an operation with a left and right identity element. (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)$$
	mgmidpfod.f	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	mgmidprnd	$$⊢\phi \to \mathrm{ran}\underset{\dot{}}{⨣}=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		mgmidpfod.f	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
6	1 2 3 4 5	mgmidpfod	$$⊢\phi \to \underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B$$
7		forn	$$⊢\underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B\to \mathrm{ran}\underset{\dot{}}{⨣}=B$$
8	6 7	syl	$$⊢\phi \to \mathrm{ran}\underset{\dot{}}{⨣}=B$$