This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 . See dftermo4 for an alternate definition using the universal property. (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 ) } )