Metamath Proof Explorer

Theorem termoval

Description: The value of the terminal object function, i.e. the set of all terminal 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 termoval ⊢φ→TermO⁡C=a∈B|∀b∈B∃!hh∈bHa

Proof

Step Hyp Ref Expression
1 initoval.c ⊢φ→C∈Cat
2 initoval.b ⊢B=BaseC
3 initoval.h ⊢H=Hom⁡C
4 df-termo ⊢TermO=c∈Cat⟼a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca
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→bHom⁡ca=bHa
10 9 eleq2d ⊢c=C→h∈bHom⁡ca↔h∈bHa
11 10 eubidv ⊢c=C→∃!hh∈bHom⁡ca↔∃!hh∈bHa
12 6 11 raleqbidv ⊢c=C→∀b∈Basec∃!hh∈bHom⁡ca↔∀b∈B∃!hh∈bHa
13 6 12 rabeqbidv ⊢c=C→a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca=a∈B|∀b∈B∃!hh∈bHa
14 2 fvexi ⊢B∈V
15 14 rabex ⊢a∈B|∀b∈B∃!hh∈bHa∈V
16 15 a1i ⊢φ→a∈B|∀b∈B∃!hh∈bHa∈V
17 4 13 1 16 fvmptd3 ⊢φ→TermO⁡C=a∈B|∀b∈B∃!hh∈bHa