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). See dftermo2 and dftermo3 for alternate definitions depending on df-inito . (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\exists !hh\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	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		va	$$setvara$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7		vb	$$setvarb$$
8		vh	$$setvarh$$
9	8	cv	$$setvarh$$
10	7	cv	$$setvarb$$
11		chom	$$class\mathrm{Hom}$$
12	5 11	cfv	$$class\mathrm{Hom}\left(c\right)$$
13	3	cv	$$setvara$$
14	10 13 12	co	$$class\left(b\mathrm{Hom}\left(c\right)a\right)$$
15	9 14	wcel	$$wffh\in \left(b\mathrm{Hom}\left(c\right)a\right)$$
16	15 8	weu	$$wff\exists !hh\in \left(b\mathrm{Hom}\left(c\right)a\right)$$
17	16 7 6	wral	$$wff\forall b\in {\mathrm{Base}}_c\exists !hh\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\exists !hh\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\exists !hh\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\exists !hh\in \left(b\mathrm{Hom}\left(c\right)a\right)\right\}\right)$$