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 ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )