Metamath Proof Explorer

Theorem oppcciceq

Description: The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypothesis oppccicb.o ⊢ O = oppCat ⁡ C
Assertion oppcciceq ⊢ ≃ 𝑐 ⁡ C = ≃ 𝑐 ⁡ O

Proof

Step Hyp Ref Expression
1 oppccicb.o ⊢ O = oppCat ⁡ C
2 cic1st2nd ⊢ p ∈ ≃ 𝑐 ⁡ C → p = 1 st ⁡ p 2 nd ⁡ p
3 cic1st2ndbr ⊢ p ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ p ≃ 𝑐 ⁡ C 2 nd ⁡ p
4 1 3 oppccic ⊢ p ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ p ≃ 𝑐 ⁡ O 2 nd ⁡ p
5 df-br ⊢ 1 st ⁡ p ≃ 𝑐 ⁡ O 2 nd ⁡ p ↔ 1 st ⁡ p 2 nd ⁡ p ∈ ≃ 𝑐 ⁡ O
6 4 5 sylib ⊢ p ∈ ≃ 𝑐 ⁡ C → 1 st ⁡ p 2 nd ⁡ p ∈ ≃ 𝑐 ⁡ O
7 2 6 eqeltrd ⊢ p ∈ ≃ 𝑐 ⁡ C → p ∈ ≃ 𝑐 ⁡ O
8 cic1st2nd ⊢ p ∈ ≃ 𝑐 ⁡ O → p = 1 st ⁡ p 2 nd ⁡ p
9 cic1st2ndbr ⊢ p ∈ ≃ 𝑐 ⁡ O → 1 st ⁡ p ≃ 𝑐 ⁡ O 2 nd ⁡ p
10 1 oppccicb ⊢ 1 st ⁡ p ≃ 𝑐 ⁡ C 2 nd ⁡ p ↔ 1 st ⁡ p ≃ 𝑐 ⁡ O 2 nd ⁡ p
11 9 10 sylibr ⊢ p ∈ ≃ 𝑐 ⁡ O → 1 st ⁡ p ≃ 𝑐 ⁡ C 2 nd ⁡ p
12 df-br ⊢ 1 st ⁡ p ≃ 𝑐 ⁡ C 2 nd ⁡ p ↔ 1 st ⁡ p 2 nd ⁡ p ∈ ≃ 𝑐 ⁡ C
13 11 12 sylib ⊢ p ∈ ≃ 𝑐 ⁡ O → 1 st ⁡ p 2 nd ⁡ p ∈ ≃ 𝑐 ⁡ C
14 8 13 eqeltrd ⊢ p ∈ ≃ 𝑐 ⁡ O → p ∈ ≃ 𝑐 ⁡ C
15 7 14 impbii ⊢ p ∈ ≃ 𝑐 ⁡ C ↔ p ∈ ≃ 𝑐 ⁡ O
16 15 eqriv ⊢ ≃ 𝑐 ⁡ C = ≃ 𝑐 ⁡ O