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 ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
2 eqid ⊢ oppCat ⁡ c = oppCat ⁡ c
3 2 oppccat ⊢ c ∈ Cat → oppCat ⁡ c ∈ Cat
4 eqid ⊢ Base c = Base c
5 2 4 oppcbas ⊢ Base c = Base oppCat ⁡ c
6 eqid ⊢ Hom ⁡ oppCat ⁡ c = Hom ⁡ oppCat ⁡ c
7 3 5 6 initoval ⊢ c ∈ Cat → InitO ⁡ oppCat ⁡ c = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ oppCat ⁡ c b
8 eqid ⊢ Hom ⁡ c = Hom ⁡ c
9 8 2 oppchom ⊢ a Hom ⁡ oppCat ⁡ c b = b Hom ⁡ c a
10 9 eleq2i ⊢ h ∈ a Hom ⁡ oppCat ⁡ c b ↔ h ∈ b Hom ⁡ c a
11 10 eubii ⊢ ∃! h h ∈ a Hom ⁡ oppCat ⁡ c b ↔ ∃! h h ∈ b Hom ⁡ c a
12 11 ralbii ⊢ ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ oppCat ⁡ c b ↔ ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
13 12 rabbii ⊢ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ oppCat ⁡ c b = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
14 7 13 eqtrdi ⊢ c ∈ Cat → InitO ⁡ oppCat ⁡ c = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
15 14 mpteq2ia ⊢ c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ c a
16 1 15 eqtr4i ⊢ TermO = c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c