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 = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctermo	|- TermO
1		vc	|- c
2		ccat	|- Cat
3		va	|- a
4		cbs	|- Base
5	1	cv	|- c
6	5 4	cfv	|- ( Base ` c )
7		vb	|- b
8		vh	|- h
9	8	cv	|- h
10	7	cv	|- b
11		chom	|- Hom
12	5 11	cfv	|- ( Hom ` c )
13	3	cv	|- a
14	10 13 12	co	|- ( b ( Hom ` c ) a )
15	9 14	wcel	|- h e. ( b ( Hom ` c ) a )
16	15 8	weu	|- E! h h e. ( b ( Hom ` c ) a )
17	16 7 6	wral	|- A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a )
18	17 3 6	crab	|- { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) }
19	1 2 18	cmpt	|- ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
20	0 19	wceq	|- TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )