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

Metamath Proof Explorer

Definition df-cmn

Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Assertion df-cmn CMnd = { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmn ⊢ CMnd
1 vg ⊢ 𝑔
2 cmnd ⊢ Mnd
3 va ⊢ 𝑎
4 cbs ⊢ Base
5 1 cv ⊢ 𝑔
6 5 4 cfv ⊢ ( Base ‘ 𝑔 )
7 vb ⊢ 𝑏
8 3 cv ⊢ 𝑎
9 cplusg ⊢ +g
10 5 9 cfv ⊢ ( +g ‘ 𝑔 )
11 7 cv ⊢ 𝑏
12 8 11 10 co ⊢ ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 )
13 11 8 10 co ⊢ ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
14 12 13 wceq ⊢ ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
15 14 7 6 wral ⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
16 15 3 6 wral ⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
17 16 1 2 crab ⊢ { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }
18 0 17 wceq ⊢ CMnd = { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }