Metamath Proof Explorer

Theorem thinchom

Description: A non-empty hom-set of a thin category is given by its element. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses thinchom.x ⊢ φ → X ∈ B
thinchom.y ⊢ φ → Y ∈ B
thinchom.f ⊢ φ → F ∈ X H Y
thinchom.b ⊢ B = Base C
thinchom.h ⊢ H = Hom ⁡ C
thinchom.c ⊢ φ → C ∈ ThinCat
Assertion thinchom ⊢ φ → X H Y = F

Proof

Step Hyp Ref Expression
1 thinchom.x ⊢ φ → X ∈ B
2 thinchom.y ⊢ φ → Y ∈ B
3 thinchom.f ⊢ φ → F ∈ X H Y
4 thinchom.b ⊢ B = Base C
5 thinchom.h ⊢ H = Hom ⁡ C
6 thinchom.c ⊢ φ → C ∈ ThinCat
7 1 adantr ⊢ φ ∧ g ∈ X H Y → X ∈ B
8 2 adantr ⊢ φ ∧ g ∈ X H Y → Y ∈ B
9 simpr ⊢ φ ∧ g ∈ X H Y → g ∈ X H Y
10 3 adantr ⊢ φ ∧ g ∈ X H Y → F ∈ X H Y
11 6 adantr ⊢ φ ∧ g ∈ X H Y → C ∈ ThinCat
12 7 8 9 10 4 5 11 thincmo2 ⊢ φ ∧ g ∈ X H Y → g = F
13 12 3 eqsnd ⊢ φ → X H Y = F