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 Could not format assertion : No typesetting found for |- EndoFMnd = ( x e. _V |-> [_ ( x ^m x ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. } ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefmnd Could not format EndoFMnd : No typesetting found for class EndoFMnd with typecode class
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 Could not format EndoFMnd = ( x e. _V |-> [_ ( x ^m x ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. } ) : No typesetting found for wff EndoFMnd = ( x e. _V |-> [_ ( x ^m x ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. } ) with typecode wff