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

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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppccic.i ⊢ ( 𝜑 → 𝑅 ( ≃𝑐 ‘ 𝐶 ) 𝑆 )
Assertion oppccic ( 𝜑 → 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )

Proof

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