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 ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
fucterm.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
fucterm.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
Assertion fucterm ( 𝜑 → 𝑄 ∈ TermCat )

Proof

Step Hyp Ref Expression
1 funcsn.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 fucterm.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 fucterm.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
4 opex ⊢ ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V
5 4 a1i ⊢ ( 𝜑 → ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10 eqid ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
11 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) )
12 2 3 6 7 8 9 10 11 functermc2 ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
13 3 termcthind ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
14 1 5 12 13 funcsn ⊢ ( 𝜑 → 𝑄 ∈ TermCat )