Metamath Proof Explorer


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