This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issmgrpOLD

Description: Obsolete version of issgrp as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis issmgrpOLD.1 
|- X = dom dom G
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 issmgrpOLD.1 
 |-  X = dom dom G
2 df-sgrOLD 
 |-  SemiGrp = ( Magma i^i Ass )
3 2 eleq2i 
 |-  ( G e. SemiGrp <-> G e. ( Magma i^i Ass ) )
4 elin 
 |-  ( G e. ( Magma i^i Ass ) <-> ( G e. Magma /\ G e. Ass ) )
5 1 ismgmOLD 
 |-  ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )
6 1 isass 
 |-  ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
7 5 6 anbi12d 
 |-  ( G e. A -> ( ( G e. Magma /\ G e. Ass ) <-> ( 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 ) ) ) ) )
8 4 7 bitrid 
 |-  ( G e. A -> ( G e. ( Magma i^i Ass ) <-> ( 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 ) ) ) ) )
9 3 8 bitrid 
 |-  ( 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 ) ) ) ) )