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

Definition df-efmnd 18680
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 19150 and symgvalstruct 19179. (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 18679 . 2 class EndoFMnd
2 vx . . 3 setvar π‘₯
3 cvv 3446 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class π‘₯
6 cmap 8766 . . . . 5 class ↑m
75, 5, 6co 7358 . . . 4 class (π‘₯ ↑m π‘₯)
8 cnx 17066 . . . . . . 7 class ndx
9 cbs 17084 . . . . . . 7 class Base
108, 9cfv 6497 . . . . . 6 class (Baseβ€˜ndx)
114cv 1541 . . . . . 6 class 𝑏
1210, 11cop 4593 . . . . 5 class ⟨(Baseβ€˜ndx), π‘βŸ©
13 cplusg 17134 . . . . . . 7 class +g
148, 13cfv 6497 . . . . . 6 class (+gβ€˜ndx)
15 vf . . . . . . 7 setvar 𝑓
16 vg . . . . . . 7 setvar 𝑔
1715cv 1541 . . . . . . . 8 class 𝑓
1816cv 1541 . . . . . . . 8 class 𝑔
1917, 18ccom 5638 . . . . . . 7 class (𝑓 ∘ 𝑔)
2015, 16, 11, 11, 19cmpo 7360 . . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
2114, 20cop 4593 . . . . 5 class ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
22 cts 17140 . . . . . . 7 class TopSet
238, 22cfv 6497 . . . . . 6 class (TopSetβ€˜ndx)
245cpw 4561 . . . . . . . . 9 class 𝒫 π‘₯
2524csn 4587 . . . . . . . 8 class {𝒫 π‘₯}
265, 25cxp 5632 . . . . . . 7 class (π‘₯ Γ— {𝒫 π‘₯})
27 cpt 17321 . . . . . . 7 class ∏t
2826, 27cfv 6497 . . . . . 6 class (∏tβ€˜(π‘₯ Γ— {𝒫 π‘₯}))
2923, 28cop 4593 . . . . 5 class ⟨(TopSetβ€˜ndx), (∏tβ€˜(π‘₯ Γ— {𝒫 π‘₯}))⟩
3012, 21, 29ctp 4591 . . . 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 5189 . 2 class (π‘₯ ∈ V ↦ ⦋(π‘₯ ↑m π‘₯) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSetβ€˜ndx), (∏tβ€˜(π‘₯ Γ— {𝒫 π‘₯}))⟩})
331, 32wceq 1542 1 wff EndoFMnd = (π‘₯ ∈ V ↦ ⦋(π‘₯ ↑m π‘₯) / π‘β¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(+gβ€˜ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSetβ€˜ndx), (∏tβ€˜(π‘₯ Γ— {𝒫 π‘₯}))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  efmnd  18681
  Copyright terms: Public domain W3C validator