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 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 } ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefmnd 
 |-  EndoFMnd
1 vx 
 |-  x
2 cvv 
 |-  _V
3 1 cv 
 |-  x
4 cmap 
 |-  ^m
5 3 3 4 co 
 |-  ( x ^m x )
6 vb 
 |-  b
7 cbs 
 |-  Base
8 cnx 
 |-  ndx
9 8 7 cfv 
 |-  ( Base ` ndx )
10 6 cv 
 |-  b
11 9 10 cop 
 |-  <. ( Base ` ndx ) , b >.
12 cplusg 
 |-  +g
13 8 12 cfv 
 |-  ( +g ` ndx )
14 vf 
 |-  f
15 vg 
 |-  g
16 14 cv 
 |-  f
17 15 cv 
 |-  g
18 16 17 ccom 
 |-  ( f o. g )
19 14 15 10 10 18 cmpo 
 |-  ( f e. b , g e. b |-> ( f o. g ) )
20 13 19 cop 
 |-  <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >.
21 cts 
 |-  TopSet
22 8 21 cfv 
 |-  ( TopSet ` ndx )
23 cpt 
 |-  Xt_
24 3 cpw 
 |-  ~P x
25 24 csn 
 |-  { ~P x }
26 3 25 cxp 
 |-  ( x X. { ~P x } )
27 26 23 cfv 
 |-  ( Xt_ ` ( x X. { ~P x } ) )
28 22 27 cop 
 |-  <. ( TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >.
29 11 20 28 ctp 
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. }
30 6 5 29 csb 
 |-  [_ ( 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 } ) ) >. }
31 1 2 30 cmpt 
 |-  ( 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 } ) ) >. } )
32 0 31 wceq 
 |-  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 } ) ) >. } )