Theorem oppccatb

Description: An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypotheses	oppccatb.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppccatb.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion	oppccatb	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝑂 ∈ Cat ) )

Proof

Step	Hyp	Ref	Expression
1		oppccatb.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppccatb.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
3	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
4		eqid	⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
5	4	oppccat	⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
6	1	2oppchomf	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
7	6	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
8	1	2oppccomf	⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
9	8	a1i	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
10		fvexd	⊢ ( 𝜑 → ( oppCat ‘ 𝑂 ) ∈ V )
11	7 9 2 10	catpropd	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ ( oppCat ‘ 𝑂 ) ∈ Cat ) )
12	5 11	imbitrrid	⊢ ( 𝜑 → ( 𝑂 ∈ Cat → 𝐶 ∈ Cat ) )
13	3 12	impbid2	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ↔ 𝑂 ∈ Cat ) )