Metamath Proof Explorer

Theorem ismndo

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 ismndo.1 
|- X = dom dom G
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 ismndo.1 
 |-  X = dom dom G
2 df-mndo 
 |-  MndOp = ( SemiGrp i^i ExId )
3 2 eleq2i 
 |-  ( G e. MndOp <-> G e. ( SemiGrp i^i ExId ) )
4 elin 
 |-  ( G e. ( SemiGrp i^i ExId ) <-> ( G e. SemiGrp /\ G e. ExId ) )
5 1 isexid 
 |-  ( G e. A -> ( G e. ExId <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )
6 5 anbi2d 
 |-  ( G e. A -> ( ( G e. SemiGrp /\ G e. ExId ) <-> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
7 4 6 bitrid 
 |-  ( G e. A -> ( G e. ( SemiGrp i^i ExId ) <-> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
8 3 7 bitrid 
 |-  ( 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 ) ) ) )