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 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
cofuterm.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
cofuterm.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐸 ) )
cofuterm.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
Assertion cofuterm ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐾 )

Proof

Step Hyp Ref Expression
1 cofuterm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2 cofuterm.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
3 cofuterm.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐸 ) )
4 cofuterm.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
5 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
6 1 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
7 6 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 5 7 4 fucterm ⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐸 ) ∈ TermCat )
9 5 fucbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ ( 𝐶 FuncCat 𝐸 ) )
10 1 2 cofucl ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
11 8 9 10 3 termcbasmo ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐾 )