Theorem mndfoOLD

Description: Obsolete version of mndfo as of 17-Aug-2026. 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, 23-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mndfoOLD.b	$$⊢B={\mathrm{Base}}_G$$
	mndfoOLD.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mndfoOLD	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		mndfoOLD.b	$$⊢B={\mathrm{Base}}_G$$
2		mndfoOLD.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		eqid	$$⊢{+}_{𝑓}\left(G\right)={+}_{𝑓}\left(G\right)$$
4	1 3	mndpfo	$$⊢G\in \mathrm{Mnd}\to {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B$$
5	4	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B$$
6	1 2 3	plusfeq	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to {+}_{𝑓}\left(G\right)=\underset{\dot{}}{+}$$
7	6	eqcomd	$$⊢\underset{\dot{}}{+}Fn\left(B\times B\right)\to \underset{\dot{}}{+}={+}_{𝑓}\left(G\right)$$
8	7	adantl	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}={+}_{𝑓}\left(G\right)$$
9		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)$$
10	8 9	syl	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \left(\underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B\leftrightarrow {+}_{𝑓}\left(G\right):B\times B\underset{onto}{⟶}B\right)$$
11	5 10	mpbird	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\right)\to \underset{\dot{}}{+}:B\times B\underset{onto}{⟶}B$$