Metamath Proof Explorer

Theorem isinito

Description: The predicate "is an initial 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 isinito ⊢φ→I∈InitO⁡C↔∀b∈B∃!hh∈IHb

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 initoval ⊢φ→InitO⁡C=i∈B|∀b∈B∃!hh∈iHb
6 5 eleq2d ⊢φ→I∈InitO⁡C↔I∈i∈B|∀b∈B∃!hh∈iHb
7 oveq1 ⊢i=I→iHb=IHb
8 7 eleq2d ⊢i=I→h∈iHb↔h∈IHb
9 8 eubidv ⊢i=I→∃!hh∈iHb↔∃!hh∈IHb
10 9 ralbidv ⊢i=I→∀b∈B∃!hh∈iHb↔∀b∈B∃!hh∈IHb
11 10 elrab3 ⊢I∈B→I∈i∈B|∀b∈B∃!hh∈iHb↔∀b∈B∃!hh∈IHb
12 4 11 syl ⊢φ→I∈i∈B|∀b∈B∃!hh∈iHb↔∀b∈B∃!hh∈IHb
13 6 12 bitrd ⊢φ→I∈InitO⁡C↔∀b∈B∃!hh∈IHb