Metamath Proof Explorer

Theorem oppctermo

Description: Terminal objects are initial in the opposite category. Comments before Definition 7.4 in Adamek p. 102. (Contributed by Zhi Wang, 26-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 termorcl ⊢ I ∈ TermO ⁡ C → C ∈ Cat
2 initorcl ⊢ I ∈ InitO ⁡ 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 initoo2 ⊢ I ∈ InitO ⁡ 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 ∈ InitO ⁡ oppCat ⁡ C → C ∈ Cat ↔ oppCat ⁡ C ∈ Cat
11 2 10 mpbird ⊢ I ∈ InitO ⁡ oppCat ⁡ C → C ∈ Cat
12 2fveq3 ⊢ c = C → InitO ⁡ oppCat ⁡ c = InitO ⁡ oppCat ⁡ C
13 dftermo2 ⊢ TermO = c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c
14 fvex ⊢ InitO ⁡ oppCat ⁡ C ∈ V
15 12 13 14 fvmpt ⊢ C ∈ Cat → TermO ⁡ C = InitO ⁡ oppCat ⁡ C
16 15 eleq2d ⊢ C ∈ Cat → I ∈ TermO ⁡ C ↔ I ∈ InitO ⁡ oppCat ⁡ C
17 1 11 16 pm5.21nii ⊢ I ∈ TermO ⁡ C ↔ I ∈ InitO ⁡ oppCat ⁡ C