Theorem mndfo

Description: 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)

	Ref	Expression
Hypotheses	mndfo.b	|- B = ( Base ` G )
	mndfo.p	|- .+ = ( +g ` G )
Assertion	mndfo	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )

Proof

Step	Hyp	Ref	Expression
1		mndfo.b	|- B = ( Base ` G )
2		mndfo.p	|- .+ = ( +g ` G )
3		eqid	|- ( +f ` G ) = ( +f ` G )
4	1 3	mndpfo	|- ( G e. Mnd -> ( +f ` G ) : ( B X. B ) -onto-> B )
5	4	adantr	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> ( +f ` G ) : ( B X. B ) -onto-> B )
6	1 2 3	plusfeq	|- ( .+ Fn ( B X. B ) -> ( +f ` G ) = .+ )
7	6	eqcomd	|- ( .+ Fn ( B X. B ) -> .+ = ( +f ` G ) )
8	7	adantl	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ = ( +f ` G ) )
9		foeq1	|- ( .+ = ( +f ` G ) -> ( .+ : ( B X. B ) -onto-> B <-> ( +f ` G ) : ( B X. B ) -onto-> B ) )
10	8 9	syl	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> ( .+ : ( B X. B ) -onto-> B <-> ( +f ` G ) : ( B X. B ) -onto-> B ) )
11	5 10	mpbird	|- ( ( G e. Mnd /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) -onto-> B )