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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinito	|- InitO
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	3	cv	|- a
11		chom	|- Hom
12	5 11	cfv	|- ( Hom ` c )
13	7	cv	|- b
14	10 13 12	co	|- ( a ( Hom ` c ) b )
15	9 14	wcel	|- h e. ( a ( Hom ` c ) b )
16	15 8	weu	|- E! h h e. ( a ( Hom ` c ) b )
17	16 7 6	wral	|- A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b )
18	17 3 6	crab	|- { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) }
19	1 2 18	cmpt	|- ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )
20	0 19	wceq	|- InitO = ( c e. Cat |-> { a e. ( Base ` c ) | A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } )