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

Metamath Proof Explorer

Theorem fucterm

Description: The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses funcsn.q ⊢ Q = C FuncCat D
fucterm.c ⊢ φ → C ∈ Cat
fucterm.d No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
Assertion fucterm Could not format assertion : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 funcsn.q ⊢ Q = C FuncCat D
2 fucterm.c ⊢ φ → C ∈ Cat
3 fucterm.d Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
4 opex ⊢ Base C × Base D x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × Base C × Base D ⁡ x Hom ⁡ D Base C × Base D ⁡ y ∈ V
5 4 a1i ⊢ φ → Base C × Base D x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × Base C × Base D ⁡ x Hom ⁡ D Base C × Base D ⁡ y ∈ V
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Base D = Base D
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 eqid ⊢ Hom ⁡ D = Hom ⁡ D
10 eqid ⊢ Base C × Base D = Base C × Base D
11 eqid ⊢ x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × Base C × Base D ⁡ x Hom ⁡ D Base C × Base D ⁡ y = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × Base C × Base D ⁡ x Hom ⁡ D Base C × Base D ⁡ y
12 2 3 6 7 8 9 10 11 functermc2 ⊢ φ → C Func D = Base C × Base D x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × Base C × Base D ⁡ x Hom ⁡ D Base C × Base D ⁡ y
13 3 termcthind ⊢ φ → D ∈ ThinCat
14 1 5 12 13 funcsn Could not format ( ph -> Q e. TermCat ) : No typesetting found for |- ( ph -> Q e. TermCat ) with typecode |-