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

Metamath Proof Explorer

Definition df-submgm

Description: A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020)

Ref Expression
Assertion df-submgm SubMgm = ( 𝑠 ∈ Mgm ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 } )

Detailed syntax breakdown

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