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

Metamath Proof Explorer

Theorem oppcterm

Description: The opposite category of a terminal category is a terminal category. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses oppcterm.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcterm.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion oppcterm ( 𝜑 → 𝑂 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 oppcterm.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcterm.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
3 1 2 oppctermhom ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )
4 1 2 oppctermco ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝑂 ) )
5 1 fvexi ⊢ 𝑂 ∈ V
6 5 a1i ⊢ ( 𝜑 → 𝑂 ∈ V )
7 3 4 2 6 termcpropd ⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝑂 ∈ TermCat ) )
8 2 7 mpbid ⊢ ( 𝜑 → 𝑂 ∈ TermCat )