Theorem thincmo2

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

	Ref	Expression
Hypotheses	isthincd2lem1.1	$$⊢\phi \to X\in B$$
	isthincd2lem1.2	$$⊢\phi \to Y\in B$$
	isthincd2lem1.3	$$⊢\phi \to F\in \left(XHY\right)$$
	isthincd2lem1.4	$$⊢\phi \to G\in \left(XHY\right)$$
	thincmo2.b	$$⊢B={\mathrm{Base}}_C$$
	thincmo2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	thincmo2.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
Assertion	thincmo2	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem1.1	$$⊢\phi \to X\in B$$
2		isthincd2lem1.2	$$⊢\phi \to Y\in B$$
3		isthincd2lem1.3	$$⊢\phi \to F\in \left(XHY\right)$$
4		isthincd2lem1.4	$$⊢\phi \to G\in \left(XHY\right)$$
5		thincmo2.b	$$⊢B={\mathrm{Base}}_C$$
6		thincmo2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
7		thincmo2.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
8	5 6	isthinc	$$⊢C\in \mathrm{ThinCat}\leftrightarrow \left(C\in \mathrm{Cat}\wedge \forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)\right)$$
9	8	simprbi	$$⊢C\in \mathrm{ThinCat}\to \forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)$$
10	7 9	syl	$$⊢\phi \to \forall x\in B\forall y\in B{\exists }^{*}ff\in \left(xHy\right)$$
11	1 2 3 4 10	isthincd2lem1	$$⊢\phi \to F=G$$