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	⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinito	⊢ InitO
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7		vb	⊢ 𝑏
8		vh	⊢ ℎ
9	8	cv	⊢ ℎ
10	3	cv	⊢ 𝑎
11		chom	⊢ Hom
12	5 11	cfv	⊢ ( Hom ‘ 𝑐 )
13	7	cv	⊢ 𝑏
14	10 13 12	co	⊢ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
15	9 14	wcel	⊢ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
16	15 8	weu	⊢ ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
17	16 7 6	wral	⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
18	17 3 6	crab	⊢ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) }
19	1 2 18	cmpt	⊢ ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
20	0 19	wceq	⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )