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

Metamath Proof Explorer

Theorem cofuterm

Description: Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses cofuterm.f ⊢ φ → F ∈ C Func D
cofuterm.g ⊢ φ → G ∈ D Func E
cofuterm.k ⊢ φ → K ∈ C Func E
cofuterm.e No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
Assertion cofuterm ⊢ φ → G ∘ func F = K

Proof

Step Hyp Ref Expression
1 cofuterm.f ⊢ φ → F ∈ C Func D
2 cofuterm.g ⊢ φ → G ∈ D Func E
3 cofuterm.k ⊢ φ → K ∈ C Func E
4 cofuterm.e Could not format ( ph -> E e. TermCat ) : No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
5 eqid ⊢ C FuncCat E = C FuncCat E
6 1 func1st2nd ⊢ φ → 1 st ⁡ F C Func D 2 nd ⁡ F
7 6 funcrcl2 ⊢ φ → C ∈ Cat
8 5 7 4 fucterm Could not format ( ph -> ( C FuncCat E ) e. TermCat ) : No typesetting found for |- ( ph -> ( C FuncCat E ) e. TermCat ) with typecode |-
9 5 fucbas ⊢ C Func E = Base C FuncCat E
10 1 2 cofucl ⊢ φ → G ∘ func F ∈ C Func E
11 8 9 10 3 termcbasmo ⊢ φ → G ∘ func F = K