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