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 
|- ( ph -> F e. ( C Func D ) )
cofuterm.g 
|- ( ph -> G e. ( D Func E ) )
cofuterm.k 
|- ( ph -> K e. ( C Func E ) )
cofuterm.e 
|- ( ph -> E e. TermCat )
Assertion cofuterm 
|- ( ph -> ( G o.func F ) = K )

Proof

Step Hyp Ref Expression
1 cofuterm.f 
 |-  ( ph -> F e. ( C Func D ) )
2 cofuterm.g 
 |-  ( ph -> G e. ( D Func E ) )
3 cofuterm.k 
 |-  ( ph -> K e. ( C Func E ) )
4 cofuterm.e 
 |-  ( ph -> E e. TermCat )
5 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
6 1 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
7 6 funcrcl2 
 |-  ( ph -> C e. Cat )
8 5 7 4 fucterm 
 |-  ( ph -> ( C FuncCat E ) e. TermCat )
9 5 fucbas 
 |-  ( C Func E ) = ( Base ` ( C FuncCat E ) )
10 1 2 cofucl 
 |-  ( ph -> ( G o.func F ) e. ( C Func E ) )
11 8 9 10 3 termcbasmo 
 |-  ( ph -> ( G o.func F ) = K )