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

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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thinchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thinchom.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
thinchom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thinchom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
thinchom.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
Assertion thinchom ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { 𝐹 } )

Proof

Step Hyp Ref Expression
1 thinchom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2 thinchom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 thinchom.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4 thinchom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
5 thinchom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 thinchom.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ∈ 𝐵 )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑌 ∈ 𝐵 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
11 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ ThinCat )
12 7 8 9 10 4 5 11 thincmo2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑔 = 𝐹 )
13 12 3 eqsnd ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = { 𝐹 } )