# 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}=\mathrm{dom}\mathrm{dom}{G}$
Assertion ismndo1 ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ismndo1.1 ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}$
2 1 ismndo ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$
3 1 smgrpmgm ${⊢}{G}\in \mathrm{SemiGrp}\to {G}:{X}×{X}⟶{X}$
4 3 ad2antrl ${⊢}\left({G}\in {A}\wedge \left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to {G}:{X}×{X}⟶{X}$
5 1 smgrpassOLD ${⊢}{G}\in \mathrm{SemiGrp}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)$
6 5 ad2antrl ${⊢}\left({G}\in {A}\wedge \left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)$
7 simprr ${⊢}\left({G}\in {A}\wedge \left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)$
8 4 6 7 3jca ${⊢}\left({G}\in {A}\wedge \left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)$
9 3simpa ${⊢}\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\to \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)$
10 1 issmgrpOLD ${⊢}{G}\in {A}\to \left({G}\in \mathrm{SemiGrp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\right)\right)$
11 9 10 syl5ibr ${⊢}{G}\in {A}\to \left(\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\to {G}\in \mathrm{SemiGrp}\right)$
12 11 imp ${⊢}\left({G}\in {A}\wedge \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to {G}\in \mathrm{SemiGrp}$
13 simpr3 ${⊢}\left({G}\in {A}\wedge \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)$
14 12 13 jca ${⊢}\left({G}\in {A}\wedge \left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)\to \left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)$
15 8 14 impbida ${⊢}{G}\in {A}\to \left(\left({G}\in \mathrm{SemiGrp}\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$
16 2 15 bitrd ${⊢}{G}\in {A}\to \left({G}\in \mathrm{MndOp}↔\left({G}:{X}×{X}⟶{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}\right){G}{z}={x}{G}\left({y}{G}{z}\right)\wedge \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{G}{y}={y}\wedge {y}{G}{x}={y}\right)\right)\right)$