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

Metamath Proof Explorer

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	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) → 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ )
3		cic1st2ndbr	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) → ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝐶 ) ( 2^nd ‘ 𝑝 ) )
4	1 3	oppccic	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) → ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝑂 ) ( 2^nd ‘ 𝑝 ) )
5		df-br	⊢ ( ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝑂 ) ( 2^nd ‘ 𝑝 ) ↔ ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ∈ ( ≃_𝑐 ‘ 𝑂 ) )
6	4 5	sylib	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) → ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ∈ ( ≃_𝑐 ‘ 𝑂 ) )
7	2 6	eqeltrd	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) → 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) )
8		cic1st2nd	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) → 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ )
9		cic1st2ndbr	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) → ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝑂 ) ( 2^nd ‘ 𝑝 ) )
10	1	oppccicb	⊢ ( ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝐶 ) ( 2^nd ‘ 𝑝 ) ↔ ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝑂 ) ( 2^nd ‘ 𝑝 ) )
11	9 10	sylibr	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) → ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝐶 ) ( 2^nd ‘ 𝑝 ) )
12		df-br	⊢ ( ( 1^st ‘ 𝑝 ) ( ≃_𝑐 ‘ 𝐶 ) ( 2^nd ‘ 𝑝 ) ↔ ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ∈ ( ≃_𝑐 ‘ 𝐶 ) )
13	11 12	sylib	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) → ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ∈ ( ≃_𝑐 ‘ 𝐶 ) )
14	8 13	eqeltrd	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) → 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) )
15	7 14	impbii	⊢ ( 𝑝 ∈ ( ≃_𝑐 ‘ 𝐶 ) ↔ 𝑝 ∈ ( ≃_𝑐 ‘ 𝑂 ) )
16	15	eqriv	⊢ ( ≃_𝑐 ‘ 𝐶 ) = ( ≃_𝑐 ‘ 𝑂 )