This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = dom dom 𝐺
Assertion ismndo ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 ∈ SemiGrp ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 ismndo.1 ⊢ 𝑋 = dom dom 𝐺
2 df-mndo ⊢ MndOp = ( SemiGrp ∩ ExId )
3 2 eleq2i ⊢ ( 𝐺 ∈ MndOp ↔ 𝐺 ∈ ( SemiGrp ∩ ExId ) )
4 elin ⊢ ( 𝐺 ∈ ( SemiGrp ∩ ExId ) ↔ ( 𝐺 ∈ SemiGrp ∧ 𝐺 ∈ ExId ) )
5 1 isexid ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ ExId ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
6 5 anbi2d ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝐺 ∈ SemiGrp ∧ 𝐺 ∈ ExId ) ↔ ( 𝐺 ∈ SemiGrp ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )
7 4 6 bitrid ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ ( SemiGrp ∩ ExId ) ↔ ( 𝐺 ∈ SemiGrp ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )
8 3 7 bitrid ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 ∈ SemiGrp ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )