Metamath Proof Explorer


Theorem ismndo1

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 ismndo1.1 X=domdomG
Assertion ismndo1 GAGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y

Proof

Step Hyp Ref Expression
1 ismndo1.1 X=domdomG
2 1 ismndo GAGMndOpGSemiGrpxXyXxGy=yyGx=y
3 1 smgrpmgm GSemiGrpG:X×XX
4 3 ad2antrl GAGSemiGrpxXyXxGy=yyGx=yG:X×XX
5 1 smgrpassOLD GSemiGrpxXyXzXxGyGz=xGyGz
6 5 ad2antrl GAGSemiGrpxXyXxGy=yyGx=yxXyXzXxGyGz=xGyGz
7 simprr GAGSemiGrpxXyXxGy=yyGx=yxXyXxGy=yyGx=y
8 4 6 7 3jca GAGSemiGrpxXyXxGy=yyGx=yG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y
9 3simpa G:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yG:X×XXxXyXzXxGyGz=xGyGz
10 1 issmgrpOLD GAGSemiGrpG:X×XXxXyXzXxGyGz=xGyGz
11 9 10 syl5ibr GAG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yGSemiGrp
12 11 imp GAG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yGSemiGrp
13 simpr3 GAG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yxXyXxGy=yyGx=y
14 12 13 jca GAG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=yGSemiGrpxXyXxGy=yyGx=y
15 8 14 impbida GAGSemiGrpxXyXxGy=yyGx=yG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y
16 2 15 bitrd GAGMndOpG:X×XXxXyXzXxGyGz=xGyGzxXyXxGy=yyGx=y