Metamath Proof Explorer

Theorem oppcinito

Description: Initial objects are terminal in the opposite category. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Assertion oppcinito ⊢ I ∈ InitO ⁡ C ↔ I ∈ TermO ⁡ oppCat ⁡ C

Proof

Step Hyp Ref Expression
1 initorcl ⊢ I ∈ InitO ⁡ C → C ∈ Cat
2 termorcl ⊢ I ∈ TermO ⁡ oppCat ⁡ C → oppCat ⁡ C ∈ Cat
3 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
4 eqid ⊢ Base C = Base C
5 3 4 oppcbas ⊢ Base C = Base oppCat ⁡ C
6 5 termoo2 ⊢ I ∈ TermO ⁡ oppCat ⁡ C → I ∈ Base C
7 elfvex ⊢ I ∈ Base C → C ∈ V
8 id ⊢ C ∈ V → C ∈ V
9 3 8 oppccatb ⊢ C ∈ V → C ∈ Cat ↔ oppCat ⁡ C ∈ Cat
10 6 7 9 3syl ⊢ I ∈ TermO ⁡ oppCat ⁡ C → C ∈ Cat ↔ oppCat ⁡ C ∈ Cat
11 2 10 mpbird ⊢ I ∈ TermO ⁡ oppCat ⁡ C → C ∈ Cat
12 2fveq3 ⊢ c = C → TermO ⁡ oppCat ⁡ c = TermO ⁡ oppCat ⁡ C
13 dfinito2 ⊢ InitO = c ∈ Cat ⟼ TermO ⁡ oppCat ⁡ c
14 fvex ⊢ TermO ⁡ oppCat ⁡ C ∈ V
15 12 13 14 fvmpt ⊢ C ∈ Cat → InitO ⁡ C = TermO ⁡ oppCat ⁡ C
16 15 eleq2d ⊢ C ∈ Cat → I ∈ InitO ⁡ C ↔ I ∈ TermO ⁡ oppCat ⁡ C
17 1 11 16 pm5.21nii ⊢ I ∈ InitO ⁡ C ↔ I ∈ TermO ⁡ oppCat ⁡ C