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

Metamath Proof Explorer

Theorem termchom

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses termchom.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
termchom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termchom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termchom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
termchom.i ⊢ 1 = ( Id ‘ 𝐶 )
Assertion termchom ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )

Proof

Step Hyp Ref Expression
1 termchom.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termchom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termchom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 termchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 termchom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 termchom.i ⊢ 1 = ( Id ‘ 𝐶 )
7 1 2 3 4 5 termchomn0 ⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )
8 neq0 ⊢ ( ¬ ( 𝑋 𝐻 𝑌 ) = ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
9 7 8 sylib ⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ∈ 𝐵 )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑌 ∈ 𝐵 )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ TermCat )
14 13 termcthind ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ ThinCat )
15 10 11 12 2 5 14 thinchom ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑋 𝐻 𝑌 ) = { 𝑓 } )
16 13 2 10 11 5 12 6 termcid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = ( 1 ‘ 𝑋 ) )
17 16 sneqd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → { 𝑓 } = { ( 1 ‘ 𝑋 ) } )
18 15 17 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )
19 9 18 exlimddv ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { ( 1 ‘ 𝑋 ) } )