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

Metamath Proof Explorer

Definition df-efmnd

Description: Define the monoid of endofunctions on set x . We represent the monoid as the set of functions from x to itself ( ( x ^m x ) ) 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 and symgvalstruct . (Contributed by AV, 25-Jan-2024)

Ref Expression
Assertion df-efmnd ⊢ EndoFMnd = x ∈ V ⟼ ⦋ x x / b⦌ Base ndx b + ndx f ∈ b , g ∈ b ⟼ f ∘ g TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefmnd class EndoFMnd
1 vx setvar x
2 cvv class V
3 1 cv setvar x
4 cmap class ↑ 𝑚
5 3 3 4 co class x x
6 vb setvar b
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 6 cv setvar b
11 9 10 cop class Base ndx b
12 cplusg class + 𝑔
13 8 12 cfv class + ndx
14 vf setvar f
15 vg setvar g
16 14 cv setvar f
17 15 cv setvar g
18 16 17 ccom class f ∘ g
19 14 15 10 10 18 cmpo class f ∈ b , g ∈ b ⟼ f ∘ g
20 13 19 cop class + ndx f ∈ b , g ∈ b ⟼ f ∘ g
21 cts class TopSet
22 8 21 cfv class TopSet ⁡ ndx
23 cpt class ∏ 𝑡
24 3 cpw class 𝒫 x
25 24 csn class 𝒫 x
26 3 25 cxp class x × 𝒫 x
27 26 23 cfv class ∏ 𝑡 ⁡ x × 𝒫 x
28 22 27 cop class TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x
29 11 20 28 ctp class Base ndx b + ndx f ∈ b , g ∈ b ⟼ f ∘ g TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x
30 6 5 29 csb class ⦋ x x / b⦌ Base ndx b + ndx f ∈ b , g ∈ b ⟼ f ∘ g TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x
31 1 2 30 cmpt class x ∈ V ⟼ ⦋ x x / b⦌ Base ndx b + ndx f ∈ b , g ∈ b ⟼ f ∘ g TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x
32 0 31 wceq wff EndoFMnd = x ∈ V ⟼ ⦋ x x / b⦌ Base ndx b + ndx f ∈ b , g ∈ b ⟼ f ∘ g TopSet ⁡ ndx ∏ 𝑡 ⁡ x × 𝒫 x