Metamath Proof Explorer

Theorem dfinito2

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

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

Proof

Step Hyp Ref Expression
1 df-inito ⊢ InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
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 termoval ⊢ c ∈ Cat → TermO ⁡ oppCat ⁡ c = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ oppCat ⁡ c a
8 eqid ⊢ Hom ⁡ c = Hom ⁡ c
9 8 2 oppchom ⊢ b Hom ⁡ oppCat ⁡ c a = a Hom ⁡ c b
10 9 eleq2i ⊢ h ∈ b Hom ⁡ oppCat ⁡ c a ↔ h ∈ a Hom ⁡ c b
11 10 eubii ⊢ ∃! h h ∈ b Hom ⁡ oppCat ⁡ c a ↔ ∃! h h ∈ a Hom ⁡ c b
12 11 ralbii ⊢ ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ oppCat ⁡ c a ↔ ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
13 12 rabbii ⊢ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ b Hom ⁡ oppCat ⁡ c a = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
14 7 13 eqtrdi ⊢ c ∈ Cat → TermO ⁡ oppCat ⁡ c = a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
15 14 mpteq2ia ⊢ c ∈ Cat ⟼ TermO ⁡ oppCat ⁡ c = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
16 1 15 eqtr4i ⊢ InitO = c ∈ Cat ⟼ TermO ⁡ oppCat ⁡ c