Theorem oppccicb

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

	Ref	Expression
Hypothesis	oppccicb.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	oppccicb	$$⊢R{\simeq }_{𝑐}\left(C\right)S\leftrightarrow R{\simeq }_{𝑐}\left(O\right)S$$

Proof

Step	Hyp	Ref	Expression
1		oppccicb.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		id	$$⊢R{\simeq }_{𝑐}\left(C\right)S\to R{\simeq }_{𝑐}\left(C\right)S$$
3	1 2	oppccic	$$⊢R{\simeq }_{𝑐}\left(C\right)S\to R{\simeq }_{𝑐}\left(O\right)S$$
4		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
5		id	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to R{\simeq }_{𝑐}\left(O\right)S$$
6	4 5	oppccic	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to R{\simeq }_{𝑐}\left(\mathrm{oppCat}\left(O\right)\right)S$$
7	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
8	7	a1i	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
9	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
10	9	a1i	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
11	8 10	cicpropd	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to {\simeq }_{𝑐}\left(C\right)={\simeq }_{𝑐}\left(\mathrm{oppCat}\left(O\right)\right)$$
12	11	breqd	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to \left(R{\simeq }_{𝑐}\left(C\right)S\leftrightarrow R{\simeq }_{𝑐}\left(\mathrm{oppCat}\left(O\right)\right)S\right)$$
13	6 12	mpbird	$$⊢R{\simeq }_{𝑐}\left(O\right)S\to R{\simeq }_{𝑐}\left(C\right)S$$
14	3 13	impbii	$$⊢R{\simeq }_{𝑐}\left(C\right)S\leftrightarrow R{\simeq }_{𝑐}\left(O\right)S$$