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 ‘ ( 𝑥 × { 𝒫 𝑥 } ) ) ⟩ } )