This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )