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	⊢ ( 𝜑 → ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )