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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctermo	⊢ TermO
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	7	cv	⊢ 𝑏
11		chom	⊢ Hom
12	5 11	cfv	⊢ ( Hom ‘ 𝑐 )
13	3	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	⊢ TermO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } )