Description: For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isinitoi.b | |
|
isinitoi.h | |
||
isinitoi.c | |
||
Assertion | termoid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isinitoi.b | |
|
2 | isinitoi.h | |
|
3 | isinitoi.c | |
|
4 | 1 2 3 | istermoi | |
5 | oveq1 | |
|
6 | 5 | eleq2d | |
7 | 6 | eubidv | |
8 | 7 | rspcv | |
9 | 8 | adantl | |
10 | eusn | |
|
11 | eqid | |
|
12 | 3 | ad2antrr | |
13 | simpr | |
|
14 | 1 2 11 12 13 | catidcl | |
15 | fvex | |
|
16 | 15 | elsn | |
17 | eqcom | |
|
18 | sneqbg | |
|
19 | 18 | bicomd | |
20 | 19 | elv | |
21 | 16 17 20 | 3bitri | |
22 | 21 | biimpi | |
23 | 22 | a1i | |
24 | eleq2 | |
|
25 | eqeq1 | |
|
26 | 23 24 25 | 3imtr4d | |
27 | 14 26 | syl5 | |
28 | 27 | exlimiv | |
29 | 28 | com12 | |
30 | 10 29 | syl5bi | |
31 | 9 30 | syld | |
32 | 31 | expimpd | |
33 | 4 32 | mpd | |