Database
BASIC CATEGORY THEORY
Categories
Initial, terminal and zero objects of a category
istermo
Next ⟩
iszeroo
Metamath Proof Explorer
Ascii
Unicode
Theorem
istermo
Description:
The predicate "is a terminal object" of a category.
(Contributed by
AV
, 3-Apr-2020)
Ref
Expression
Hypotheses
isinito.b
⊢
B
=
Base
C
isinito.h
⊢
H
=
Hom
⁡
C
isinito.c
⊢
φ
→
C
∈
Cat
isinito.i
⊢
φ
→
I
∈
B
Assertion
istermo
⊢
φ
→
I
∈
TermO
⁡
C
↔
∀
b
∈
B
∃!
h
h
∈
b
H
I
Proof
Step
Hyp
Ref
Expression
1
isinito.b
⊢
B
=
Base
C
2
isinito.h
⊢
H
=
Hom
⁡
C
3
isinito.c
⊢
φ
→
C
∈
Cat
4
isinito.i
⊢
φ
→
I
∈
B
5
3
1
2
termoval
⊢
φ
→
TermO
⁡
C
=
i
∈
B
|
∀
b
∈
B
∃!
h
h
∈
b
H
i
6
5
eleq2d
⊢
φ
→
I
∈
TermO
⁡
C
↔
I
∈
i
∈
B
|
∀
b
∈
B
∃!
h
h
∈
b
H
i
7
oveq2
⊢
i
=
I
→
b
H
i
=
b
H
I
8
7
eleq2d
⊢
i
=
I
→
h
∈
b
H
i
↔
h
∈
b
H
I
9
8
eubidv
⊢
i
=
I
→
∃!
h
h
∈
b
H
i
↔
∃!
h
h
∈
b
H
I
10
9
ralbidv
⊢
i
=
I
→
∀
b
∈
B
∃!
h
h
∈
b
H
i
↔
∀
b
∈
B
∃!
h
h
∈
b
H
I
11
10
elrab3
⊢
I
∈
B
→
I
∈
i
∈
B
|
∀
b
∈
B
∃!
h
h
∈
b
H
i
↔
∀
b
∈
B
∃!
h
h
∈
b
H
I
12
4
11
syl
⊢
φ
→
I
∈
i
∈
B
|
∀
b
∈
B
∃!
h
h
∈
b
H
i
↔
∀
b
∈
B
∃!
h
h
∈
b
H
I
13
6
12
bitrd
⊢
φ
→
I
∈
TermO
⁡
C
↔
∀
b
∈
B
∃!
h
h
∈
b
H
I