Description: Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal objects, see statement in Lang p. 58 ("... if P, P' are two universal objects [... then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 18-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | termoeu1.c | |
|
termoeu1.a | |
||
termoeu1.b | |
||
Assertion | termoeu1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | termoeu1.c | |
|
2 | termoeu1.a | |
|
3 | termoeu1.b | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 4 5 1 | istermoi | |
7 | 3 6 | mpdan | |
8 | 4 5 1 | istermoi | |
9 | 2 8 | mpdan | |
10 | oveq1 | |
|
11 | 10 | eleq2d | |
12 | 11 | eubidv | |
13 | 12 | rspcv | |
14 | eqid | |
|
15 | 1 | adantr | |
16 | simprl | |
|
17 | simprr | |
|
18 | 4 5 14 15 16 17 | isohom | |
19 | 18 | adantr | |
20 | euex | |
|
21 | 20 | a1i | |
22 | oveq1 | |
|
23 | 22 | eleq2d | |
24 | 23 | eubidv | |
25 | 24 | rspcva | |
26 | euex | |
|
27 | 25 26 | syl | |
28 | 27 | ex | |
29 | 28 | ad2antll | |
30 | eqid | |
|
31 | 15 | ad2antrr | |
32 | 16 | ad2antrr | |
33 | 17 | ad2antrr | |
34 | 1 2 3 | 2termoinv | |
35 | 34 | ad4ant134 | |
36 | 4 30 31 32 33 14 35 | inviso1 | |
37 | 36 | ex | |
38 | 37 | eximdv | |
39 | 38 | expcom | |
40 | 39 | exlimiv | |
41 | 40 | com3l | |
42 | 41 | impd | |
43 | 21 29 42 | syl2and | |
44 | 43 | imp | |
45 | simprl | |
|
46 | euelss | |
|
47 | 19 44 45 46 | syl3anc | |
48 | 47 | exp42 | |
49 | 48 | com24 | |
50 | 49 | com14 | |
51 | 50 | expd | |
52 | 13 51 | syldc | |
53 | 52 | com15 | |
54 | 53 | impd | |
55 | 9 54 | mpd | |
56 | 55 | impd | |
57 | 7 56 | mpd | |