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	⊢ ( 𝜑 → 𝑅 ( ≃𝑐 ‘ 𝑂 ) 𝑆 )