Metamath Proof Explorer

Theorem dftermo2

Description: A terminal object is an initial object in the opposite category. An alternate definition of df-termo depending on df-inito . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo2 ⊢TermO=c∈Cat⟼InitO⁡oppCat⁡c

Proof

Step Hyp Ref Expression
1 df-termo ⊢TermO=c∈Cat⟼a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca
2 eqid ⊢oppCat⁡c=oppCat⁡c
3 2 oppccat ⊢c∈Cat→oppCat⁡c∈Cat
4 eqid ⊢Basec=Basec
5 2 4 oppcbas ⊢Basec=BaseoppCat⁡c
6 eqid ⊢Hom⁡oppCat⁡c=Hom⁡oppCat⁡c
7 3 5 6 initoval ⊢c∈Cat→InitO⁡oppCat⁡c=a∈Basec|∀b∈Basec∃!hh∈aHom⁡oppCat⁡cb
8 eqid ⊢Hom⁡c=Hom⁡c
9 8 2 oppchom ⊢aHom⁡oppCat⁡cb=bHom⁡ca
10 9 eleq2i ⊢h∈aHom⁡oppCat⁡cb↔h∈bHom⁡ca
11 10 eubii ⊢∃!hh∈aHom⁡oppCat⁡cb↔∃!hh∈bHom⁡ca
12 11 ralbii ⊢∀b∈Basec∃!hh∈aHom⁡oppCat⁡cb↔∀b∈Basec∃!hh∈bHom⁡ca
13 12 rabbii ⊢a∈Basec|∀b∈Basec∃!hh∈aHom⁡oppCat⁡cb=a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca
14 7 13 eqtrdi ⊢c∈Cat→InitO⁡oppCat⁡c=a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca
15 14 mpteq2ia ⊢c∈Cat⟼InitO⁡oppCat⁡c=c∈Cat⟼a∈Basec|∀b∈Basec∃!hh∈bHom⁡ca
16 1 15 eqtr4i ⊢TermO=c∈Cat⟼InitO⁡oppCat⁡c