Metamath Proof Explorer


Theorem termoeu1

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 φCCat
termoeu1.a φATermOC
termoeu1.b φBTermOC
Assertion termoeu1 φ∃!ffAIsoCB

Proof

Step Hyp Ref Expression
1 termoeu1.c φCCat
2 termoeu1.a φATermOC
3 termoeu1.b φBTermOC
4 eqid BaseC=BaseC
5 eqid HomC=HomC
6 4 5 1 istermoi φBTermOCBBaseCaBaseC∃!ffaHomCB
7 3 6 mpdan φBBaseCaBaseC∃!ffaHomCB
8 4 5 1 istermoi φATermOCABaseCbBaseC∃!ggbHomCA
9 2 8 mpdan φABaseCbBaseC∃!ggbHomCA
10 oveq1 a=AaHomCB=AHomCB
11 10 eleq2d a=AfaHomCBfAHomCB
12 11 eubidv a=A∃!ffaHomCB∃!ffAHomCB
13 12 rspcv ABaseCaBaseC∃!ffaHomCB∃!ffAHomCB
14 eqid IsoC=IsoC
15 1 adantr φABaseCBBaseCCCat
16 simprl φABaseCBBaseCABaseC
17 simprr φABaseCBBaseCBBaseC
18 4 5 14 15 16 17 isohom φABaseCBBaseCAIsoCBAHomCB
19 18 adantr φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCAAIsoCBAHomCB
20 euex ∃!ffAHomCBffAHomCB
21 20 a1i φABaseCBBaseC∃!ffAHomCBffAHomCB
22 oveq1 b=BbHomCA=BHomCA
23 22 eleq2d b=BgbHomCAgBHomCA
24 23 eubidv b=B∃!ggbHomCA∃!ggBHomCA
25 24 rspcva BBaseCbBaseC∃!ggbHomCA∃!ggBHomCA
26 euex ∃!ggBHomCAggBHomCA
27 25 26 syl BBaseCbBaseC∃!ggbHomCAggBHomCA
28 27 ex BBaseCbBaseC∃!ggbHomCAggBHomCA
29 28 ad2antll φABaseCBBaseCbBaseC∃!ggbHomCAggBHomCA
30 eqid InvC=InvC
31 15 ad2antrr φABaseCBBaseCgBHomCAfAHomCBCCat
32 16 ad2antrr φABaseCBBaseCgBHomCAfAHomCBABaseC
33 17 ad2antrr φABaseCBBaseCgBHomCAfAHomCBBBaseC
34 1 2 3 2termoinv φgBHomCAfAHomCBfAInvCBg
35 34 ad4ant134 φABaseCBBaseCgBHomCAfAHomCBfAInvCBg
36 4 30 31 32 33 14 35 inviso1 φABaseCBBaseCgBHomCAfAHomCBfAIsoCB
37 36 ex φABaseCBBaseCgBHomCAfAHomCBfAIsoCB
38 37 eximdv φABaseCBBaseCgBHomCAffAHomCBffAIsoCB
39 38 expcom gBHomCAφABaseCBBaseCffAHomCBffAIsoCB
40 39 exlimiv ggBHomCAφABaseCBBaseCffAHomCBffAIsoCB
41 40 com3l φABaseCBBaseCffAHomCBggBHomCAffAIsoCB
42 41 impd φABaseCBBaseCffAHomCBggBHomCAffAIsoCB
43 21 29 42 syl2and φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCAffAIsoCB
44 43 imp φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCAffAIsoCB
45 simprl φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCA∃!ffAHomCB
46 euelss AIsoCBAHomCBffAIsoCB∃!ffAHomCB∃!ffAIsoCB
47 19 44 45 46 syl3anc φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCA∃!ffAIsoCB
48 47 exp42 φABaseCBBaseC∃!ffAHomCBbBaseC∃!ggbHomCA∃!ffAIsoCB
49 48 com24 φ∃!ffAHomCBbBaseC∃!ggbHomCABBaseCABaseC∃!ffAIsoCB
50 49 com14 ABaseC∃!ffAHomCBbBaseC∃!ggbHomCABBaseCφ∃!ffAIsoCB
51 50 expd ABaseC∃!ffAHomCBbBaseC∃!ggbHomCABBaseCφ∃!ffAIsoCB
52 13 51 syldc aBaseC∃!ffaHomCBABaseCbBaseC∃!ggbHomCABBaseCφ∃!ffAIsoCB
53 52 com15 φABaseCbBaseC∃!ggbHomCABBaseCaBaseC∃!ffaHomCB∃!ffAIsoCB
54 53 impd φABaseCbBaseC∃!ggbHomCABBaseCaBaseC∃!ffaHomCB∃!ffAIsoCB
55 9 54 mpd φBBaseCaBaseC∃!ffaHomCB∃!ffAIsoCB
56 55 impd φBBaseCaBaseC∃!ffaHomCB∃!ffAIsoCB
57 7 56 mpd φ∃!ffAIsoCB