Metamath Proof Explorer

Theorem ismndo1

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

Ref Expression
Hypothesis ismndo1.1
`|- X = dom dom G`
Assertion ismndo1
`|- ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`

Proof

Step Hyp Ref Expression
1 ismndo1.1
` |-  X = dom dom G`
2 1 ismndo
` |-  ( G e. A -> ( G e. MndOp <-> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`
3 1 smgrpmgm
` |-  ( G e. SemiGrp -> G : ( X X. X ) --> X )`
` |-  ( ( G e. A /\ ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> G : ( X X. X ) --> X )`
5 1 smgrpassOLD
` |-  ( G e. SemiGrp -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) )`
` |-  ( ( G e. A /\ ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) )`
7 simprr
` |-  ( ( G e. A /\ ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) )`
8 4 6 7 3jca
` |-  ( ( G e. A /\ ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )`
9 3simpa
` |-  ( ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) -> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )`
10 1 issmgrpOLD
` |-  ( G e. A -> ( G e. SemiGrp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )`
11 9 10 syl5ibr
` |-  ( G e. A -> ( ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) -> G e. SemiGrp ) )`
12 11 imp
` |-  ( ( G e. A /\ ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> G e. SemiGrp )`
13 simpr3
` |-  ( ( G e. A /\ ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) )`
14 12 13 jca
` |-  ( ( G e. A /\ ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) -> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )`
15 8 14 impbida
` |-  ( G e. A -> ( ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`
16 2 15 bitrd
` |-  ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`