# Metamath Proof Explorer

## Theorem ismndo2

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 ismndo2.1
`|- X = ran G`
Assertion ismndo2
`|- ( 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 ismndo2.1
` |-  X = ran G`
2 mndomgmid
` |-  ( G e. MndOp -> G e. ( Magma i^i ExId ) )`
3 rngopidOLD
` |-  ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )`
4 2 3 syl
` |-  ( G e. MndOp -> ran G = dom dom G )`
5 1 4 syl5eq
` |-  ( G e. MndOp -> X = dom dom G )`
6 5 a1i
` |-  ( G e. A -> ( G e. MndOp -> X = dom dom G ) )`
7 fdm
` |-  ( G : ( X X. X ) --> X -> dom G = ( X X. X ) )`
8 7 dmeqd
` |-  ( G : ( X X. X ) --> X -> dom dom G = dom ( X X. X ) )`
9 dmxpid
` |-  dom ( X X. X ) = X`
10 8 9 syl6req
` |-  ( G : ( X X. X ) --> X -> X = dom dom G )`
` |-  ( ( 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 ) ) -> X = dom dom G )`
12 11 a1i
` |-  ( 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 ) ) -> X = dom dom G ) )`
13 eqid
` |-  dom dom G = dom dom G`
14 13 ismndo1
` |-  ( G e. A -> ( G e. MndOp <-> ( G : ( dom dom G X. dom dom G ) --> dom dom G /\ A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. dom dom G A. y e. dom dom G ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`
15 xpid11
` |-  ( ( X X. X ) = ( dom dom G X. dom dom G ) <-> X = dom dom G )`
16 15 biimpri
` |-  ( X = dom dom G -> ( X X. X ) = ( dom dom G X. dom dom G ) )`
17 feq23
` |-  ( ( ( X X. X ) = ( dom dom G X. dom dom G ) /\ X = dom dom G ) -> ( G : ( X X. X ) --> X <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) )`
18 16 17 mpancom
` |-  ( X = dom dom G -> ( G : ( X X. X ) --> X <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) )`
19 raleq
` |-  ( X = dom dom G -> ( A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )`
20 19 raleqbi1dv
` |-  ( X = dom dom G -> ( A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )`
21 20 raleqbi1dv
` |-  ( X = dom dom G -> ( A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )`
22 raleq
` |-  ( X = dom dom G -> ( A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) <-> A. y e. dom dom G ( ( x G y ) = y /\ ( y G x ) = y ) ) )`
23 22 rexeqbi1dv
` |-  ( X = dom dom G -> ( E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) <-> E. x e. dom dom G A. y e. dom dom G ( ( x G y ) = y /\ ( y G x ) = y ) ) )`
24 18 21 23 3anbi123d
` |-  ( X = dom dom G -> ( ( 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 : ( dom dom G X. dom dom G ) --> dom dom G /\ A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. dom dom G A. y e. dom dom G ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )`
25 24 bibi2d
` |-  ( X = dom dom G -> ( ( 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 ) ) ) <-> ( G e. MndOp <-> ( G : ( dom dom G X. dom dom G ) --> dom dom G /\ A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. dom dom G A. y e. dom dom G ( ( x G y ) = y /\ ( y G x ) = y ) ) ) ) )`
26 14 25 syl5ibrcom
` |-  ( G e. A -> ( X = dom dom G -> ( 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 ) ) ) ) )`
27 6 12 26 pm5.21ndd
` |-  ( 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 ) ) ) )`