Definition df-inito

Description: An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in Adamek p. 101, or definition in Lang p. 57 (called "a universally repelling object" there). See dfinito2 and dfinito3 for alternate definitions depending on df-termo . (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Assertion	df-inito	$$⊢\mathrm{InitO}=\left(c\in \mathrm{Cat}⟼\left\{a\in {\mathrm{Base}}_c|\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(a\mathrm{Hom}\left(c\right)b\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinito	$$class\mathrm{InitO}$$
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	3	cv	$$setvara$$
11		chom	$$class\mathrm{Hom}$$
12	5 11	cfv	$$class\mathrm{Hom}\left(c\right)$$
13	7	cv	$$setvarb$$
14	10 13 12	co	$$class\left(a\mathrm{Hom}\left(c\right)b\right)$$
15	9 14	wcel	$$wffh\in \left(a\mathrm{Hom}\left(c\right)b\right)$$
16	15 8	weu	$$wff\exists !hh\in \left(a\mathrm{Hom}\left(c\right)b\right)$$
17	16 7 6	wral	$$wff\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(a\mathrm{Hom}\left(c\right)b\right)$$
18	17 3 6	crab	$$class\left\{a\in {\mathrm{Base}}_c|\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(a\mathrm{Hom}\left(c\right)b\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(a\mathrm{Hom}\left(c\right)b\right)\right\}\right)$$
20	0 19	wceq	$$wff\mathrm{InitO}=\left(c\in \mathrm{Cat}⟼\left\{a\in {\mathrm{Base}}_c|\forall b\in {\mathrm{Base}}_c\exists !hh\in \left(a\mathrm{Hom}\left(c\right)b\right)\right\}\right)$$