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
|
syl5bb |
|- ( 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
|
syl5bb |
|- ( 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 ) ) ) ) |