Definition df-inito 18164

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 18183 and dfinito3 18185 for alternate definitions depending on df-termo 18165. See dfinito4 50729 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020.)

Assertion

Ref	Expression
df-inito	⊢ InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})

Distinct variable group:   𝑎,𝑏,𝑐,ℎ

Detailed syntax breakdown of Definition df-inito

Step	Hyp	Ref	Expression
1		cinito 18161	. 2 class InitO
2		vc	. . 3 setvar 𝑐
3		ccat 17843	. . 3 class Cat
4		vh	. . . . . . . 8 setvar ℎ
5	4	cv 1568	. . . . . . 7 class ℎ
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1568	. . . . . . . 8 class 𝑎
8		vb	. . . . . . . . 9 setvar 𝑏
9	8	cv 1568	. . . . . . . 8 class 𝑏
10	2	cv 1568	. . . . . . . . 9 class 𝑐
11		chom 17444	. . . . . . . . 9 class Hom
12	10, 11	cfv 6538	. . . . . . . 8 class (Hom ‘𝑐)
13	7, 9, 12	co 7420	. . . . . . 7 class (𝑎(Hom ‘𝑐)𝑏)
14	5, 13	wcel 2144	. . . . . 6 wff ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)
15	14, 4	weu 2593	. . . . 5 wff ∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)
16		cbs 17392	. . . . . 6 class Base
17	10, 16	cfv 6538	. . . . 5 class (Base‘𝑐)
18	15, 8, 17	wral 3076	. . . 4 wff ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)
19	18, 6, 17	crab 3412	. . 3 class {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)}
20	2, 3, 19	cmpt 5185	. 2 class (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})
21	1, 20	wceq 1569	1 wff InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃!ℎ ℎ ∈ (𝑎(Hom ‘𝑐)𝑏)})

This definition is used by:  initofn  18167  initorcl  18170  initoval  18173  dfinito2  18183