Metamath Proof Explorer

Theorem oppcthin

Description: The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypothesis oppcthin.o ⊢ O = oppCat ⁡ C
Assertion oppcthin ⊢ C ∈ ThinCat → O ∈ ThinCat

Proof

Step Hyp Ref Expression
1 oppcthin.o ⊢ O = oppCat ⁡ C
2 eqid ⊢ Base C = Base C
3 1 2 oppcbas ⊢ Base C = Base O
4 3 a1i ⊢ C ∈ ThinCat → Base C = Base O
5 eqidd ⊢ C ∈ ThinCat → Hom ⁡ O = Hom ⁡ O
6 simpl ⊢ C ∈ ThinCat ∧ x ∈ Base C ∧ y ∈ Base C → C ∈ ThinCat
7 simprr ⊢ C ∈ ThinCat ∧ x ∈ Base C ∧ y ∈ Base C → y ∈ Base C
8 simprl ⊢ C ∈ ThinCat ∧ x ∈ Base C ∧ y ∈ Base C → x ∈ Base C
9 eqid ⊢ Hom ⁡ C = Hom ⁡ C
10 6 7 8 2 9 thincmo ⊢ C ∈ ThinCat ∧ x ∈ Base C ∧ y ∈ Base C → ∃* f f ∈ y Hom ⁡ C x
11 9 1 oppchom ⊢ x Hom ⁡ O y = y Hom ⁡ C x
12 11 eleq2i ⊢ f ∈ x Hom ⁡ O y ↔ f ∈ y Hom ⁡ C x
13 12 mobii ⊢ ∃* f f ∈ x Hom ⁡ O y ↔ ∃* f f ∈ y Hom ⁡ C x
14 10 13 sylibr ⊢ C ∈ ThinCat ∧ x ∈ Base C ∧ y ∈ Base C → ∃* f f ∈ x Hom ⁡ O y
15 thinccat ⊢ C ∈ ThinCat → C ∈ Cat
16 1 oppccat ⊢ C ∈ Cat → O ∈ Cat
17 15 16 syl ⊢ C ∈ ThinCat → O ∈ Cat
18 4 5 14 17 isthincd ⊢ C ∈ ThinCat → O ∈ ThinCat