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