Description: Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-endval.c | |
|
bj-endval.x | |
||
Assertion | bj-endval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-endval.c | |
|
2 | bj-endval.x | |
|
3 | df-bj-end | |
|
4 | fveq2 | |
|
5 | fveq2 | |
|
6 | 5 | oveqd | |
7 | 6 | opeq2d | |
8 | fveq2 | |
|
9 | 8 | oveqd | |
10 | 9 | opeq2d | |
11 | 7 10 | preq12d | |
12 | 4 11 | mpteq12dv | |
13 | fvex | |
|
14 | 13 | mptex | |
15 | 14 | a1i | |
16 | 3 12 1 15 | fvmptd3 | |
17 | id | |
|
18 | 17 17 | oveq12d | |
19 | 18 | opeq2d | |
20 | 17 17 | opeq12d | |
21 | 20 17 | oveq12d | |
22 | 21 | opeq2d | |
23 | 19 22 | preq12d | |
24 | 23 | adantl | |
25 | prex | |
|
26 | 25 | a1i | |
27 | 16 24 2 26 | fvmptd | |