Description: The monoid of endofunctions on a set A is a topological monoid. Formerly part of proof for symgtgp . (Contributed by AV, 23-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | efmndtmd.g | No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |- | |
Assertion | efmndtmd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efmndtmd.g | Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |- | |
2 | 1 | efmndmnd | |
3 | eqid | |
|
4 | 1 3 | efmndtopn | |
5 | distopon | |
|
6 | eqid | |
|
7 | 6 | pttoponconst | |
8 | 5 7 | mpdan | |
9 | 1 3 | efmndbas | |
10 | 9 | eleq2i | |
11 | 10 | biimpi | |
12 | 11 | a1i | |
13 | 12 | ssrdv | |
14 | resttopon | |
|
15 | 8 13 14 | syl2anc | |
16 | 4 15 | eqeltrrd | |
17 | eqid | |
|
18 | 3 17 | istps | |
19 | 16 18 | sylibr | |
20 | eqid | |
|
21 | 1 3 20 | efmndplusg | |
22 | eqid | |
|
23 | distop | |
|
24 | eqid | |
|
25 | 24 | xkotopon | |
26 | 23 23 25 | syl2anc | |
27 | cndis | |
|
28 | 5 27 | mpdan | |
29 | 13 28 | sseqtrrd | |
30 | disllycmp | |
|
31 | llynlly | |
|
32 | 30 31 | syl | |
33 | eqid | |
|
34 | 33 | xkococn | |
35 | 23 32 23 34 | syl3anc | |
36 | 22 26 29 22 26 29 35 | cnmpt2res | |
37 | 21 36 | eqeltrid | |
38 | xkopt | |
|
39 | 23 38 | mpancom | |
40 | 39 | oveq1d | |
41 | 40 4 | eqtrd | |
42 | 41 41 | oveq12d | |
43 | 42 | oveq1d | |
44 | 37 43 | eleqtrd | |
45 | vex | |
|
46 | vex | |
|
47 | 45 46 | coex | |
48 | 21 47 | fnmpoi | |
49 | eqid | |
|
50 | 3 20 49 | plusfeq | |
51 | 48 50 | ax-mp | |
52 | 51 | eqcomi | |
53 | 3 52 | mndplusf | |
54 | frn | |
|
55 | 2 53 54 | 3syl | |
56 | cnrest2 | |
|
57 | 26 55 29 56 | syl3anc | |
58 | 44 57 | mpbid | |
59 | 41 | oveq2d | |
60 | 58 59 | eleqtrd | |
61 | 52 17 | istmd | |
62 | 2 19 60 61 | syl3anbrc | |