Description: Obsolete version of sgrpass as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | smgrpassOLD.1 | |- X = dom dom G |
|
| Assertion | 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 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | smgrpassOLD.1 | |- X = dom dom G |
|
| 2 | 1 | issmgrpOLD | |- ( G e. SemiGrp -> ( 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 ) ) ) ) ) |
| 3 | simpr | |- ( ( 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 ) ) ) -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) |
|
| 4 | 2 3 | biimtrdi | |- ( G e. SemiGrp -> ( 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 ) ) ) ) |
| 5 | 4 | pm2.43i | |- ( 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 ) ) ) |