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

Metamath Proof Explorer

Theorem functermceu

Description: There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses functermceu.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
functermceu.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
Assertion functermceu ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 functermceu.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 functermceu.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3 opex ⊢ ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V
4 3 a1i ⊢ ( 𝜑 → ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 eqid ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
10 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) )
11 1 2 5 6 7 8 9 10 functermc2 ⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
12 sneq ⊢ ( 𝑓 = ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ → { 𝑓 } = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
13 12 eqeq2d ⊢ ( 𝑓 = ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ → ( ( 𝐶 Func 𝐷 ) = { 𝑓 } ↔ ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } ) )
14 4 11 13 spcedv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
15 eusn ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↔ ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
16 14 15 sylibr ⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )