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

Metamath Proof Explorer

Definition df-submnd

Description: A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Assertion df-submnd SubMnd = ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubmnd ⊢ SubMnd
1 vs ⊢ 𝑠
2 cmnd ⊢ Mnd
3 vt ⊢ 𝑡
4 cbs ⊢ Base
5 1 cv ⊢ 𝑠
6 5 4 cfv ⊢ ( Base ‘ 𝑠 )
7 6 cpw ⊢ 𝒫 ( Base ‘ 𝑠 )
8 c0g ⊢ 0g
9 5 8 cfv ⊢ ( 0g ‘ 𝑠 )
10 3 cv ⊢ 𝑡
11 9 10 wcel ⊢ ( 0g ‘ 𝑠 ) ∈ 𝑡
12 vx ⊢ 𝑥
13 vy ⊢ 𝑦
14 12 cv ⊢ 𝑥
15 cplusg ⊢ +g
16 5 15 cfv ⊢ ( +g ‘ 𝑠 )
17 13 cv ⊢ 𝑦
18 14 17 16 co ⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 )
19 18 10 wcel ⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
20 19 13 10 wral ⊢ ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
21 20 12 10 wral ⊢ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡
22 11 21 wa ⊢ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 )
23 22 3 7 crab ⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) }
24 1 2 23 cmpt ⊢ ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )
25 0 24 wceq ⊢ SubMnd = ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )