Theorem thincmo2

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

	Ref	Expression
Hypotheses	isthincd2lem1.1	|- ( ph -> X e. B )
	isthincd2lem1.2	|- ( ph -> Y e. B )
	isthincd2lem1.3	|- ( ph -> F e. ( X H Y ) )
	isthincd2lem1.4	|- ( ph -> G e. ( X H Y ) )
	thincmo2.b	|- B = ( Base ` C )
	thincmo2.h	|- H = ( Hom ` C )
	thincmo2.c	|- ( ph -> C e. ThinCat )
Assertion	thincmo2	|- ( ph -> F = G )

Proof

Step	Hyp	Ref	Expression
1		isthincd2lem1.1	|- ( ph -> X e. B )
2		isthincd2lem1.2	|- ( ph -> Y e. B )
3		isthincd2lem1.3	|- ( ph -> F e. ( X H Y ) )
4		isthincd2lem1.4	|- ( ph -> G e. ( X H Y ) )
5		thincmo2.b	|- B = ( Base ` C )
6		thincmo2.h	|- H = ( Hom ` C )
7		thincmo2.c	|- ( ph -> C e. ThinCat )
8	5 6	isthinc	|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )
9	8	simprbi	|- ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) )
10	7 9	syl	|- ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
11	1 2 3 4 10	isthincd2lem1	|- ( ph -> F = G )