Metamath Proof Explorer

Theorem initoval

Description: The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses initoval.c ⊢φ→C∈Cat
initoval.b ⊢B=BaseC
initoval.h ⊢H=Hom⁡C
Assertion initoval ⊢φ→InitO⁡C=a∈B|∀b∈B∃!hh∈aHb

Proof

Step Hyp Ref Expression
1 initoval.c ⊢φ→C∈Cat
2 initoval.b ⊢B=BaseC
3 initoval.h ⊢H=Hom⁡C
4 df-inito ⊢InitO=c∈Cat⟼a∈Basec|∀b∈Basec∃!hh∈aHom⁡cb
5 fveq2 ⊢c=C→Basec=BaseC
6 5 2 eqtr4di ⊢c=C→Basec=B
7 fveq2 ⊢c=C→Hom⁡c=Hom⁡C
8 7 3 eqtr4di ⊢c=C→Hom⁡c=H
9 8 oveqd ⊢c=C→aHom⁡cb=aHb
10 9 eleq2d ⊢c=C→h∈aHom⁡cb↔h∈aHb
11 10 eubidv ⊢c=C→∃!hh∈aHom⁡cb↔∃!hh∈aHb
12 6 11 raleqbidv ⊢c=C→∀b∈Basec∃!hh∈aHom⁡cb↔∀b∈B∃!hh∈aHb
13 6 12 rabeqbidv ⊢c=C→a∈Basec|∀b∈Basec∃!hh∈aHom⁡cb=a∈B|∀b∈B∃!hh∈aHb
14 2 fvexi ⊢B∈V
15 14 rabex ⊢a∈B|∀b∈B∃!hh∈aHb∈V
16 15 a1i ⊢φ→a∈B|∀b∈B∃!hh∈aHb∈V
17 4 13 1 16 fvmptd3 ⊢φ→InitO⁡C=a∈B|∀b∈B∃!hh∈aHb