# Metamath Proof Explorer

## Theorem grpomndo

Description: A group is a monoid. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion grpomndo
`|- ( G e. GrpOp -> G e. MndOp )`

### Proof

Step Hyp Ref Expression
1 eqid
` |-  ran G = ran G`
2 1 isgrpo
` |-  ( G e. GrpOp -> ( G e. GrpOp <-> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) ) )`
3 2 biimpd
` |-  ( G e. GrpOp -> ( G e. GrpOp -> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) ) )`
4 1 grpoidinv
` |-  ( G e. GrpOp -> E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) )`
5 simpl
` |-  ( ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> ( ( x G y ) = y /\ ( y G x ) = y ) )`
6 5 ralimi
` |-  ( A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) )`
7 6 reximi
` |-  ( E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) )`
8 1 ismndo2
` |-  ( G e. GrpOp -> ( G e. MndOp <-> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`
9 8 biimprcd
` |-  ( ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) ) -> ( G e. GrpOp -> G e. MndOp ) )`
10 9 3exp
` |-  ( G : ( ran G X. ran G ) --> ran G -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> G e. MndOp ) ) ) )`
11 10 impcom
` |-  ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> G e. MndOp ) ) )`
12 11 com3l
` |-  ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) ) )`
13 7 12 syl
` |-  ( E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) ) )`
14 4 13 mpcom
` |-  ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) )`
15 14 expdcom
` |-  ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( G : ( ran G X. ran G ) --> ran G -> ( G e. GrpOp -> G e. MndOp ) ) )`
16 15 a1i
` |-  ( E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( G : ( ran G X. ran G ) --> ran G -> ( G e. GrpOp -> G e. MndOp ) ) ) )`
17 16 com13
` |-  ( G : ( ran G X. ran G ) --> ran G -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) -> ( G e. GrpOp -> G e. MndOp ) ) ) )`
18 17 3imp
` |-  ( ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) -> ( G e. GrpOp -> G e. MndOp ) )`
19 3 18 syli
` |-  ( G e. GrpOp -> ( G e. GrpOp -> G e. MndOp ) )`
20 19 pm2.43i
` |-  ( G e. GrpOp -> G e. MndOp )`