Theorem oppccicb

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

	Ref	Expression
Hypothesis	oppccicb.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion	oppccicb	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		oppccicb.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		id	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 )
3	1 2	oppccic	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 → 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )
4		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
5		id	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )
6	4 5	oppccic	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → 𝑅 ( ≃𝑐 ‘ ( oppCat ‘ 𝑂 ) ) 𝑆 )
7	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
8	7	a1i	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
9	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
10	9	a1i	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
11	8 10	cicpropd	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → ( ≃𝑐 ‘ 𝐶 ) = ( ≃𝑐 ‘ ( oppCat ‘ 𝑂 ) ) )
12	11	breqd	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ 𝑅 ( ≃𝑐 ‘ ( oppCat ‘ 𝑂 ) ) 𝑆 ) )
13	6 12	mpbird	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 )
14	3 13	impbii	⊢ ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )