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 ⊢ 𝑂 = ( 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 ⊢ ( 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 ↔ 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )