# Metamath Proof Explorer

## Definition df-termo

Description: An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in Adamek p. 102, or definition in Lang p. 57 (called "a universally attracting object" there). (Contributed by AV, 3-Apr-2020)

Ref Expression
Assertion df-termo ${⊢}\mathrm{TermO}=\left({c}\in \mathrm{Cat}⟼\left\{{a}\in {\mathrm{Base}}_{{c}}|\forall {b}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ctermo ${class}\mathrm{TermO}$
1 vc ${setvar}{c}$
2 ccat ${class}\mathrm{Cat}$
3 va ${setvar}{a}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{c}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{c}}$
7 vb ${setvar}{b}$
8 vh ${setvar}{h}$
9 8 cv ${setvar}{h}$
10 7 cv ${setvar}{b}$
11 chom ${class}\mathrm{Hom}$
12 5 11 cfv ${class}\mathrm{Hom}\left({c}\right)$
13 3 cv ${setvar}{a}$
14 10 13 12 co ${class}\left({b}\mathrm{Hom}\left({c}\right){a}\right)$
15 9 14 wcel ${wff}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)$
16 15 8 weu ${wff}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)$
17 16 7 6 wral ${wff}\forall {b}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)$
18 17 3 6 crab ${class}\left\{{a}\in {\mathrm{Base}}_{{c}}|\forall {b}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)\right\}$
19 1 2 18 cmpt ${class}\left({c}\in \mathrm{Cat}⟼\left\{{a}\in {\mathrm{Base}}_{{c}}|\forall {b}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)\right\}\right)$
20 0 19 wceq ${wff}\mathrm{TermO}=\left({c}\in \mathrm{Cat}⟼\left\{{a}\in {\mathrm{Base}}_{{c}}|\forall {b}\in {\mathrm{Base}}_{{c}}\phantom{\rule{.4em}{0ex}}\exists !{h}\phantom{\rule{.4em}{0ex}}{h}\in \left({b}\mathrm{Hom}\left({c}\right){a}\right)\right\}\right)$