Theorem thincmo2

Description: Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthincd2lem1.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	isthincd2lem1.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	isthincd2lem1.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	isthincd2lem1.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
	thincmo2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	thincmo2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	thincmo2.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
Assertion	thincmo2	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem1.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2		isthincd2lem1.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3		isthincd2lem1.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		isthincd2lem1.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
5		thincmo2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
6		thincmo2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
7		thincmo2.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
8	5 6	isthinc	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
9	8	simprbi	⊢ ( 𝐶 ∈ ThinCat → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
10	7 9	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
11	1 2 3 4 10	isthincd2lem1	⊢ ( 𝜑 → 𝐹 = 𝐺 )