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 No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
termchom.b ⊢ B = Base C
termchom.x ⊢ φ → X ∈ B
termchom.y ⊢ φ → Y ∈ B
termchom.h ⊢ H = Hom ⁡ C
termchom.i ⊢ 1 ˙ = Id ⁡ C
Assertion termchom ⊢ φ → X H Y = 1 ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 termchom.c Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2 termchom.b ⊢ B = Base C
3 termchom.x ⊢ φ → X ∈ B
4 termchom.y ⊢ φ → Y ∈ B
5 termchom.h ⊢ H = Hom ⁡ C
6 termchom.i ⊢ 1 ˙ = Id ⁡ C
7 1 2 3 4 5 termchomn0 ⊢ φ → ¬ X H Y = ∅
8 neq0 ⊢ ¬ X H Y = ∅ ↔ ∃ f f ∈ X H Y
9 7 8 sylib ⊢ φ → ∃ f f ∈ X H Y
10 3 adantr ⊢ φ ∧ f ∈ X H Y → X ∈ B
11 4 adantr ⊢ φ ∧ f ∈ X H Y → Y ∈ B
12 simpr ⊢ φ ∧ f ∈ X H Y → f ∈ X H Y
13 1 adantr Could not format ( ( ph /\ f e. ( X H Y ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ f e. ( X H Y ) ) -> C e. TermCat ) with typecode |-
14 13 termcthind ⊢ φ ∧ f ∈ X H Y → C ∈ ThinCat
15 10 11 12 2 5 14 thinchom ⊢ φ ∧ f ∈ X H Y → X H Y = f
16 13 2 10 11 5 12 6 termcid ⊢ φ ∧ f ∈ X H Y → f = 1 ˙ ⁡ X
17 16 sneqd ⊢ φ ∧ f ∈ X H Y → f = 1 ˙ ⁡ X
18 15 17 eqtrd ⊢ φ ∧ f ∈ X H Y → X H Y = 1 ˙ ⁡ X
19 9 18 exlimddv ⊢ φ → X H Y = 1 ˙ ⁡ X