Definition df-termo 16642

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). (Contributed by AV, 3-Apr-2020.)

Assertion

Ref	Expression
df-termo	|- TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )

Distinct variable group:   a, b, c, h

Detailed syntax breakdown of Definition df-termo

Step	Hyp	Ref	Expression
1		ctermo 16639	. 2 class TermO
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vh	. . . . . . . 8 setvar h
5	4	cv 1482	. . . . . . 7 class h
6		vb	. . . . . . . . 9 setvar b
7	6	cv 1482	. . . . . . . 8 class b
8		va	. . . . . . . . 9 setvar a
9	8	cv 1482	. . . . . . . 8 class a
10	2	cv 1482	. . . . . . . . 9 class c
11		chom 15952	. . . . . . . . 9 class Hom
12	10, 11	cfv 5888	. . . . . . . 8 class ( Hom ` c )
13	7, 9, 12	co 6650	. . . . . . 7 class ( b ( Hom ` c ) a )
14	5, 13	wcel 1990	. . . . . 6 wff h e. ( b ( Hom ` c ) a )
15	14, 4	weu 2470	. . . . 5 wff E! h h e. ( b ( Hom ` c ) a )
16		cbs 15857	. . . . . 6 class Base
17	10, 16	cfv 5888	. . . . 5 class ( Base ` c )
18	15, 6, 17	wral 2912	. . . 4 wff A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a )
19	18, 8, 17	crab 2916	. . 3 class { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) }
20	2, 3, 19	cmpt 4729	. 2 class ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )
21	1, 20	wceq 1483	1 wff TermO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } )

This definition is referenced by:  termorcl  16645  termoval  16648