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

Metamath Proof Explorer

Theorem termchom2

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 21-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
termchom2.z ⊢ φ → Z ∈ B
Assertion termchom2 ⊢ φ → X H Y = 1 ˙ ⁡ Z

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 termchom2.z ⊢ φ → Z ∈ B
8 1 2 3 4 5 6 termchom ⊢ φ → X H Y = 1 ˙ ⁡ X
9 1 2 3 7 termcbasmo ⊢ φ → X = Z
10 9 fveq2d ⊢ φ → 1 ˙ ⁡ X = 1 ˙ ⁡ Z
11 10 sneqd ⊢ φ → 1 ˙ ⁡ X = 1 ˙ ⁡ Z
12 8 11 eqtrd ⊢ φ → X H Y = 1 ˙ ⁡ Z