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 eqtrid 
 |-  ( 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 eqtr2di 
 |-  ( G : ( X X. X ) --> X -> X = dom dom G )
11 10 3ad2ant1 
 |-  ( ( 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 ) ) ) )