Metamath Proof Explorer

Theorem oppccatb

Description: An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Hypotheses oppccatb.o ⊢ O = oppCat ⁡ C
oppccatb.c ⊢ φ → C ∈ V
Assertion oppccatb ⊢ φ → C ∈ Cat ↔ O ∈ Cat

Proof

Step Hyp Ref Expression
1 oppccatb.o ⊢ O = oppCat ⁡ C
2 oppccatb.c ⊢ φ → C ∈ V
3 1 oppccat ⊢ C ∈ Cat → O ∈ Cat
4 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
5 4 oppccat ⊢ O ∈ Cat → oppCat ⁡ O ∈ Cat
6 1 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
7 6 a1i ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
8 1 2oppccomf ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
9 8 a1i ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
10 fvexd ⊢ φ → oppCat ⁡ O ∈ V
11 7 9 2 10 catpropd ⊢ φ → C ∈ Cat ↔ oppCat ⁡ O ∈ Cat
12 5 11 imbitrrid ⊢ φ → O ∈ Cat → C ∈ Cat
13 3 12 impbid2 ⊢ φ → C ∈ Cat ↔ O ∈ Cat