Metamath Proof Explorer

Theorem oppccic

Description: Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Hypotheses oppccic.o ⊢ O = oppCat ⁡ C
oppccic.i ⊢ φ → R ≃ 𝑐 ⁡ C S
Assertion oppccic ⊢ φ → R ≃ 𝑐 ⁡ O S

Proof

Step Hyp Ref Expression
1 oppccic.o ⊢ O = oppCat ⁡ C
2 oppccic.i ⊢ φ → R ≃ 𝑐 ⁡ C S
3 cicrcl2 ⊢ R ≃ 𝑐 ⁡ C S → C ∈ Cat
4 2 3 syl ⊢ φ → C ∈ Cat
5 1 oppccat ⊢ C ∈ Cat → O ∈ Cat
6 4 5 syl ⊢ φ → O ∈ Cat
7 eqid ⊢ Base C = Base C
8 cicrcl ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → S ∈ Base C
9 4 2 8 syl2anc ⊢ φ → S ∈ Base C
10 ciclcl ⊢ C ∈ Cat ∧ R ≃ 𝑐 ⁡ C S → R ∈ Base C
11 4 2 10 syl2anc ⊢ φ → R ∈ Base C
12 eqid ⊢ Iso ⁡ C = Iso ⁡ C
13 eqid ⊢ Iso ⁡ O = Iso ⁡ O
14 7 1 4 9 11 12 13 oppciso ⊢ φ → S Iso ⁡ O R = R Iso ⁡ C S
15 14 neeq1d ⊢ φ → S Iso ⁡ O R ≠ ∅ ↔ R Iso ⁡ C S ≠ ∅
16 1 7 oppcbas ⊢ Base C = Base O
17 13 16 6 9 11 brcic ⊢ φ → S ≃ 𝑐 ⁡ O R ↔ S Iso ⁡ O R ≠ ∅
18 12 7 4 11 9 brcic ⊢ φ → R ≃ 𝑐 ⁡ C S ↔ R Iso ⁡ C S ≠ ∅
19 15 17 18 3bitr4rd ⊢ φ → R ≃ 𝑐 ⁡ C S ↔ S ≃ 𝑐 ⁡ O R
20 2 19 mpbid ⊢ φ → S ≃ 𝑐 ⁡ O R
21 cicsym ⊢ O ∈ Cat ∧ S ≃ 𝑐 ⁡ O R → R ≃ 𝑐 ⁡ O S
22 6 20 21 syl2anc ⊢ φ → R ≃ 𝑐 ⁡ O S