Metamath Proof Explorer

Theorem imasmndf1

Description: The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasmndf1.u 
|- U = ( F "s R )
imasmndf1.v 
|- V = ( Base ` R )
Assertion imasmndf1 
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> U e. Mnd )

Proof

Step Hyp Ref Expression
1 imasmndf1.u 
 |-  U = ( F "s R )
2 imasmndf1.v 
 |-  V = ( Base ` R )
3 1 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> U = ( F "s R ) )
4 2 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> V = ( Base ` R ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 f1f1orn 
 |-  ( F : V -1-1-> B -> F : V -1-1-onto-> ran F )
7 6 adantr 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> F : V -1-1-onto-> ran F )
8 f1ofo 
 |-  ( F : V -1-1-onto-> ran F -> F : V -onto-> ran F )
9 7 8 syl 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> F : V -onto-> ran F )
10 7 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Mnd ) /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
11 simpr 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> R e. Mnd )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 3 4 5 9 10 11 12 imasmnd 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> ( U e. Mnd /\ ( F ` ( 0g ` R ) ) = ( 0g ` U ) ) )
14 13 simpld 
 |-  ( ( F : V -1-1-> B /\ R e. Mnd ) -> U e. Mnd )