Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-efmnd Structured version   Visualization version   GIF version

Definition df-efmnd 18009
 Description: Define the monoid of endofunctions on set 𝑥. We represent the monoid as the set of functions from 𝑥 to itself ((𝑥 ↑m 𝑥)) under function composition, and topologize it as a function space assuming the set is discrete. Analogous to the former definition of SymGrp, see df-symg 18471 and symgvalstruct 18500. (Contributed by AV, 25-Jan-2024.)
Assertion
Ref Expression
df-efmnd EndoFMnd = (𝑥 ∈ V ↦ (𝑥m 𝑥) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,𝑥

Detailed syntax breakdown of Definition df-efmnd
StepHypRef Expression
1 cefmnd 18008 . 2 class EndoFMnd
2 vx . . 3 setvar 𝑥
3 cvv 3470 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1536 . . . . 5 class 𝑥
6 cmap 8380 . . . . 5 class m
75, 5, 6co 7129 . . . 4 class (𝑥m 𝑥)
8 cnx 16455 . . . . . . 7 class ndx
9 cbs 16458 . . . . . . 7 class Base
108, 9cfv 6327 . . . . . 6 class (Base‘ndx)
114cv 1536 . . . . . 6 class 𝑏
1210, 11cop 4545 . . . . 5 class ⟨(Base‘ndx), 𝑏
13 cplusg 16540 . . . . . . 7 class +g
148, 13cfv 6327 . . . . . 6 class (+g‘ndx)
15 vf . . . . . . 7 setvar 𝑓
16 vg . . . . . . 7 setvar 𝑔
1715cv 1536 . . . . . . . 8 class 𝑓
1816cv 1536 . . . . . . . 8 class 𝑔
1917, 18ccom 5531 . . . . . . 7 class (𝑓𝑔)
2015, 16, 11, 11, 19cmpo 7131 . . . . . 6 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))
2114, 20cop 4545 . . . . 5 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩
22 cts 16546 . . . . . . 7 class TopSet
238, 22cfv 6327 . . . . . 6 class (TopSet‘ndx)
245cpw 4511 . . . . . . . . 9 class 𝒫 𝑥
2524csn 4539 . . . . . . . 8 class {𝒫 𝑥}
265, 25cxp 5525 . . . . . . 7 class (𝑥 × {𝒫 𝑥})
27 cpt 16687 . . . . . . 7 class t
2826, 27cfv 6327 . . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
2923, 28cop 4545 . . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
3012, 21, 29ctp 4543 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
314, 7, 30csb 3856 . . 3 class (𝑥m 𝑥) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
322, 3, 31cmpt 5118 . 2 class (𝑥 ∈ V ↦ (𝑥m 𝑥) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
331, 32wceq 1537 1 wff EndoFMnd = (𝑥 ∈ V ↦ (𝑥m 𝑥) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
 Colors of variables: wff setvar class This definition is referenced by:  efmnd  18010
 Copyright terms: Public domain W3C validator