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=BaseC
isinito.h ⊢H=Hom⁡C
isinito.c ⊢φ→C∈Cat
isinito.i ⊢φ→I∈B
Assertion istermo ⊢φ→I∈TermO⁡C↔∀b∈B∃!hh∈bHI

Proof

Step Hyp Ref Expression
1 isinito.b ⊢B=BaseC
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∃!hh∈bHi
6 5 eleq2d ⊢φ→I∈TermO⁡C↔I∈i∈B|∀b∈B∃!hh∈bHi
7 oveq2 ⊢i=I→bHi=bHI
8 7 eleq2d ⊢i=I→h∈bHi↔h∈bHI
9 8 eubidv ⊢i=I→∃!hh∈bHi↔∃!hh∈bHI
10 9 ralbidv ⊢i=I→∀b∈B∃!hh∈bHi↔∀b∈B∃!hh∈bHI
11 10 elrab3 ⊢I∈B→I∈i∈B|∀b∈B∃!hh∈bHi↔∀b∈B∃!hh∈bHI
12 4 11 syl ⊢φ→I∈i∈B|∀b∈B∃!hh∈bHi↔∀b∈B∃!hh∈bHI
13 6 12 bitrd ⊢φ→I∈TermO⁡C↔∀b∈B∃!hh∈bHI