Theorem mgmidpfod

Description: The operation of a magma with identity as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (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	mgmidpfod	$$⊢\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		mgmidpfod.f	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
6	1 5	mgmplusf	$$⊢G\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
7	3 6	syl	$$⊢\phi \to \underset{\dot{}}{⨣}:B\times B⟶B$$
8	1 2 5	plusfval	$$⊢\left(e\in B\wedge x\in B\right)\to e\underset{\dot{}}{⨣}x=e\underset{\dot{}}{+}x$$
9	8	adantll	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x\in B\right)\to e\underset{\dot{}}{⨣}x=e\underset{\dot{}}{+}x$$
10	9	eqeq1d	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x\in B\right)\to \left(e\underset{\dot{}}{⨣}x=x\leftrightarrow e\underset{\dot{}}{+}x=x\right)$$
11	10	anbi1d	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x\in B\right)\to \left(\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
12	11	ralbidva	$$⊢\left(\phi \wedge e\in B\right)\to \left(\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
13	12	rexbidva	$$⊢\phi \to \left(\exists e\in B\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
14	4 13	mpbird	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
15		simpl	$$⊢\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to e\underset{\dot{}}{⨣}x=x$$
16	15	ralimi	$$⊢\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \forall x\in Be\underset{\dot{}}{⨣}x=x$$
17		oveq2	$$⊢x=y\to e\underset{\dot{}}{⨣}x=e\underset{\dot{}}{⨣}y$$
18		id	$$⊢x=y\to x=y$$
19	17 18	eqeq12d	$$⊢x=y\to \left(e\underset{\dot{}}{⨣}x=x\leftrightarrow e\underset{\dot{}}{⨣}y=y\right)$$
20	19	rspcv	$$⊢y\in B\to \left(\forall x\in Be\underset{\dot{}}{⨣}x=x\to e\underset{\dot{}}{⨣}y=y\right)$$
21		eqcom	$$⊢y=e\underset{\dot{}}{⨣}x\leftrightarrow e\underset{\dot{}}{⨣}x=y$$
22	17	eqeq1d	$$⊢x=y\to \left(e\underset{\dot{}}{⨣}x=y\leftrightarrow e\underset{\dot{}}{⨣}y=y\right)$$
23	21 22	bitrid	$$⊢x=y\to \left(y=e\underset{\dot{}}{⨣}x\leftrightarrow e\underset{\dot{}}{⨣}y=y\right)$$
24	23	rspcev	$$⊢\left(y\in B\wedge e\underset{\dot{}}{⨣}y=y\right)\to \exists x\in By=e\underset{\dot{}}{⨣}x$$
25	24	ex	$$⊢y\in B\to \left(e\underset{\dot{}}{⨣}y=y\to \exists x\in By=e\underset{\dot{}}{⨣}x\right)$$
26	20 25	syld	$$⊢y\in B\to \left(\forall x\in Be\underset{\dot{}}{⨣}x=x\to \exists x\in By=e\underset{\dot{}}{⨣}x\right)$$
27	16 26	syl5	$$⊢y\in B\to \left(\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \exists x\in By=e\underset{\dot{}}{⨣}x\right)$$
28	27	reximdv	$$⊢y\in B\to \left(\exists e\in B\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \exists e\in B\exists x\in By=e\underset{\dot{}}{⨣}x\right)$$
29	28	impcom	$$⊢\left(\exists e\in B\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\wedge y\in B\right)\to \exists e\in B\exists x\in By=e\underset{\dot{}}{⨣}x$$
30	29	ralrimiva	$$⊢\exists e\in B\forall x\in B\left(e\underset{\dot{}}{⨣}x=x\wedge x\underset{\dot{}}{+}e=x\right)\to \forall y\in B\exists e\in B\exists x\in By=e\underset{\dot{}}{⨣}x$$
31	14 30	syl	$$⊢\phi \to \forall y\in B\exists e\in B\exists x\in By=e\underset{\dot{}}{⨣}x$$
32		foov	$$⊢\underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B\leftrightarrow \left(\underset{\dot{}}{⨣}:B\times B⟶B\wedge \forall y\in B\exists e\in B\exists x\in By=e\underset{\dot{}}{⨣}x\right)$$
33	7 31 32	sylanbrc	$$⊢\phi \to \underset{\dot{}}{⨣}:B\times B\underset{onto}{⟶}B$$