Theorem oppcciceq

Description: The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oppccicb.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		cic1st2nd	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
3		cic1st2ndbr	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) → ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑝 ) )
4	1 3	oppccic	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) → ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝑂 ) ( 2nd ‘ 𝑝 ) )
5		df-br	⊢ ( ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝑂 ) ( 2nd ‘ 𝑝 ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ≃𝑐 ‘ 𝑂 ) )
6	4 5	sylib	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) → ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ≃𝑐 ‘ 𝑂 ) )
7	2 6	eqeltrd	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) → 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) )
8		cic1st2nd	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
9		cic1st2ndbr	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) → ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝑂 ) ( 2nd ‘ 𝑝 ) )
10	1	oppccicb	⊢ ( ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑝 ) ↔ ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝑂 ) ( 2nd ‘ 𝑝 ) )
11	9 10	sylibr	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) → ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑝 ) )
12		df-br	⊢ ( ( 1st ‘ 𝑝 ) ( ≃𝑐 ‘ 𝐶 ) ( 2nd ‘ 𝑝 ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ≃𝑐 ‘ 𝐶 ) )
13	11 12	sylib	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) → ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ≃𝑐 ‘ 𝐶 ) )
14	8 13	eqeltrd	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) → 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) )
15	7 14	impbii	⊢ ( 𝑝 ∈ ( ≃𝑐 ‘ 𝐶 ) ↔ 𝑝 ∈ ( ≃𝑐 ‘ 𝑂 ) )
16	15	eqriv	⊢ ( ≃𝑐 ‘ 𝐶 ) = ( ≃𝑐 ‘ 𝑂 )