Definition df-inito 16641

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

Assertion

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

Distinct variable group:   a, b, c, h

Detailed syntax breakdown of Definition df-inito

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

This definition is referenced by:  initorcl  16644  initoval  16647