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 = dom ⁡ dom ⁡ G
Assertion ismndo1 ⊢ G ∈ A → G ∈ MndOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y

Proof

Step Hyp Ref Expression
1 ismndo1.1 ⊢ X = dom ⁡ dom ⁡ G
2 1 ismndo ⊢ G ∈ A → G ∈ MndOp ↔ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
3 1 smgrpmgm ⊢ G ∈ SemiGrp → G : X × X ⟶ X
4 3 ad2antrl ⊢ G ∈ A ∧ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G : X × X ⟶ X
5 1 smgrpassOLD ⊢ G ∈ SemiGrp → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
6 5 ad2antrl ⊢ G ∈ A ∧ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
7 simprr ⊢ G ∈ A ∧ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
8 4 6 7 3jca ⊢ G ∈ A ∧ G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
9 3simpa ⊢ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
10 1 issmgrpOLD ⊢ G ∈ A → G ∈ SemiGrp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z
11 9 10 syl5ibr ⊢ G ∈ A → G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G ∈ SemiGrp
12 11 imp ⊢ G ∈ A ∧ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G ∈ SemiGrp
13 simpr3 ⊢ G ∈ A ∧ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
14 12 13 jca ⊢ G ∈ A ∧ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y → G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
15 8 14 impbida ⊢ G ∈ A → G ∈ SemiGrp ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y
16 2 15 bitrd ⊢ G ∈ A → G ∈ MndOp ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∀ y ∈ X ∀ z ∈ X x G y G z = x G y G z ∧ ∃ x ∈ X ∀ y ∈ X x G y = y ∧ y G x = y