This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppccicb

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

Ref Expression
Hypothesis oppccicb.o ⊢ O = oppCat ⁡ C
Assertion oppccicb ⊢ R ≃ 𝑐 ⁡ C S ↔ R ≃ 𝑐 ⁡ O S

Proof

Step Hyp Ref Expression
1 oppccicb.o ⊢ O = oppCat ⁡ C
2 id ⊢ R ≃ 𝑐 ⁡ C S → R ≃ 𝑐 ⁡ C S
3 1 2 oppccic ⊢ R ≃ 𝑐 ⁡ C S → R ≃ 𝑐 ⁡ O S
4 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
5 id ⊢ R ≃ 𝑐 ⁡ O S → R ≃ 𝑐 ⁡ O S
6 4 5 oppccic ⊢ R ≃ 𝑐 ⁡ O S → R ≃ 𝑐 ⁡ oppCat ⁡ O S
7 1 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
8 7 a1i ⊢ R ≃ 𝑐 ⁡ O S → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
9 1 2oppccomf ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
10 9 a1i ⊢ R ≃ 𝑐 ⁡ O S → comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
11 8 10 cicpropd ⊢ R ≃ 𝑐 ⁡ O S → ≃ 𝑐 ⁡ C = ≃ 𝑐 ⁡ oppCat ⁡ O
12 11 breqd ⊢ R ≃ 𝑐 ⁡ O S → R ≃ 𝑐 ⁡ C S ↔ R ≃ 𝑐 ⁡ oppCat ⁡ O S
13 6 12 mpbird ⊢ R ≃ 𝑐 ⁡ O S → R ≃ 𝑐 ⁡ C S
14 3 13 impbii ⊢ R ≃ 𝑐 ⁡ C S ↔ R ≃ 𝑐 ⁡ O S