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	No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
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	Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
8	5 6	isthinc	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) ) with typecode |-
9	8	simprbi	Could not format ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) : No typesetting found for |- ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) ) with typecode |-
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$$