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 = ( Base ` G )
	mgmidpfod.p	|- .+ = ( +g ` G )
	mgmidpfod.g	|- ( ph -> G e. Mgm )
	mgmidpfod.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
	mgmfod.f	|- ( ph -> .+ Fn ( B X. B ) )
Assertion	mgmfod	|- ( ph -> .+ : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		mgmidpfod.b	|- B = ( Base ` G )
2		mgmidpfod.p	|- .+ = ( +g ` G )
3		mgmidpfod.g	|- ( ph -> G e. Mgm )
4		mgmidpfod.e	|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
5		mgmfod.f	|- ( ph -> .+ Fn ( B X. B ) )
6		eqid	|- ( +f ` G ) = ( +f ` G )
7	1 2 3 4 6	mgmidpfod	|- ( ph -> ( +f ` G ) : ( B X. B ) -onto-> B )
8	1 2 6	plusfeq	|- ( .+ Fn ( B X. B ) -> ( +f ` G ) = .+ )
9	5 8	syl	|- ( ph -> ( +f ` G ) = .+ )
10	9	eqcomd	|- ( ph -> .+ = ( +f ` G ) )
11		foeq1	|- ( .+ = ( +f ` G ) -> ( .+ : ( B X. B ) -onto-> B <-> ( +f ` G ) : ( B X. B ) -onto-> B ) )
12	10 11	syl	|- ( ph -> ( .+ : ( B X. B ) -onto-> B <-> ( +f ` G ) : ( B X. B ) -onto-> B ) )
13	7 12	mpbird	|- ( ph -> .+ : ( B X. B ) -onto-> B )