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 ⊢ O = oppCat ⁡ C
oppcterm.c No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
Assertion oppcterm Could not format assertion : No typesetting found for |- ( ph -> O e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 oppcterm.o ⊢ O = oppCat ⁡ C
2 oppcterm.c Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
3 1 2 oppctermhom ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
4 1 2 oppctermco ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ O
5 1 fvexi ⊢ O ∈ V
6 5 a1i ⊢ φ → O ∈ V
7 3 4 2 6 termcpropd Could not format ( ph -> ( C e. TermCat <-> O e. TermCat ) ) : No typesetting found for |- ( ph -> ( C e. TermCat <-> O e. TermCat ) ) with typecode |-
8 2 7 mpbid Could not format ( ph -> O e. TermCat ) : No typesetting found for |- ( ph -> O e. TermCat ) with typecode |-