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

Metamath Proof Explorer

Theorem thincmo

Description: There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses thincmo.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincmo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincmo.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion thincmo ( 𝜑 → ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )

Proof

Step Hyp Ref Expression
1 thincmo.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3 thincmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 thincmo.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
5 thincmo.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
7 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑌 ∈ 𝐵 )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
9 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝐶 ∈ ThinCat )
11 6 7 8 9 4 5 10 thincmo2 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) ) → 𝑓 = 𝑔 )
12 11 ex ⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = 𝑔 ) )
13 12 alrimivv ⊢ ( 𝜑 → ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = 𝑔 ) )
14 eleq1w ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↔ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) )
15 14 mo4 ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↔ ∀ 𝑓 ∀ 𝑔 ( ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑔 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 = 𝑔 ) )
16 13 15 sylibr ⊢ ( 𝜑 → ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )