Description: The set of injective endofunctions on a set A is a submonoid of the monoid of endofunctions on A . (Contributed by AV, 25-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sursubmefmnd.m | No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |- | |
Assertion | injsubmefmnd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sursubmefmnd.m | Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |- | |
2 | vex | |
|
3 | f1eq1 | |
|
4 | 2 3 | elab | |
5 | f1f | |
|
6 | eqid | |
|
7 | 1 6 | elefmndbas | |
8 | 5 7 | syl5ibr | |
9 | 4 8 | syl5bi | |
10 | 9 | ssrdv | |
11 | 1 | efmndid | |
12 | resiexg | |
|
13 | f1oi | |
|
14 | f1of1 | |
|
15 | 13 14 | mp1i | |
16 | f1eq1 | |
|
17 | 12 15 16 | elabd | |
18 | 11 17 | eqeltrrd | |
19 | vex | |
|
20 | f1eq1 | |
|
21 | 19 20 | elab | |
22 | 4 21 | anbi12i | |
23 | f1co | |
|
24 | 23 | adantl | |
25 | f1f | |
|
26 | 5 25 | anim12i | |
27 | 1 6 | elefmndbas | |
28 | 7 27 | anbi12d | |
29 | 26 28 | syl5ibr | |
30 | 29 | imp | |
31 | eqid | |
|
32 | 1 6 31 | efmndov | |
33 | 30 32 | syl | |
34 | 33 | eleq1d | |
35 | 2 19 | coex | |
36 | f1eq1 | |
|
37 | 35 36 | elab | |
38 | 34 37 | bitrdi | |
39 | 24 38 | mpbird | |
40 | 39 | ex | |
41 | 22 40 | syl5bi | |
42 | 41 | ralrimivv | |
43 | 1 | efmndmnd | |
44 | eqid | |
|
45 | 6 44 31 | issubm | |
46 | 43 45 | syl | |
47 | 10 18 42 46 | mpbir3and | |