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

Metamath Proof Explorer

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 ) )