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 = ( 𝑥 ∈ V ↦ ( 𝑥m 𝑥 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cefmnd EndoFMnd
1 vx 𝑥
2 cvv V
3 1 cv 𝑥
4 cmap m
5 3 3 4 co ( 𝑥m 𝑥 )
6 vb 𝑏
7 cbs Base
8 cnx ndx
9 8 7 cfv ( Base ‘ ndx )
10 6 cv 𝑏
11 9 10 cop ⟨ ( Base ‘ ndx ) , 𝑏
12 cplusg +g
13 8 12 cfv ( +g ‘ ndx )
14 vf 𝑓
15 vg 𝑔
16 14 cv 𝑓
17 15 cv 𝑔
18 16 17 ccom ( 𝑓𝑔 )
19 14 15 10 10 18 cmpo ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) )
20 13 19 cop ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩
21 cts TopSet
22 8 21 cfv ( TopSet ‘ ndx )
23 cpt t
24 3 cpw 𝒫 𝑥
25 24 csn { 𝒫 𝑥 }
26 3 25 cxp ( 𝑥 × { 𝒫 𝑥 } )
27 26 23 cfv ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) )
28 22 27 cop ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩
29 11 20 28 ctp { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ }
30 6 5 29 csb ( 𝑥m 𝑥 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ }
31 1 2 30 cmpt ( 𝑥 ∈ V ↦ ( 𝑥m 𝑥 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ } )
32 0 31 wceq EndoFMnd = ( 𝑥 ∈ V ↦ ( 𝑥m 𝑥 ) / 𝑏 { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓𝑏 , 𝑔𝑏 ↦ ( 𝑓𝑔 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ } )