Metamath Proof Explorer


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 ) } )