Theorem thincmod

Description: At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024)

	Ref	Expression
Hypotheses	thincmo.c	|- ( ph -> C e. ThinCat )
	thincmo.x	|- ( ph -> X e. B )
	thincmo.y	|- ( ph -> Y e. B )
	thincn0eu.b	|- ( ph -> B = ( Base ` C ) )
	thincn0eu.h	|- ( ph -> H = ( Hom ` C ) )
Assertion	thincmod	|- ( ph -> E* f f e. ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		thincmo.c	|- ( ph -> C e. ThinCat )
2		thincmo.x	|- ( ph -> X e. B )
3		thincmo.y	|- ( ph -> Y e. B )
4		thincn0eu.b	|- ( ph -> B = ( Base ` C ) )
5		thincn0eu.h	|- ( ph -> H = ( Hom ` C ) )
6	2 4	eleqtrd	|- ( ph -> X e. ( Base ` C ) )
7	3 4	eleqtrd	|- ( ph -> Y e. ( Base ` C ) )
8		eqid	|- ( Base ` C ) = ( Base ` C )
9		eqid	|- ( Hom ` C ) = ( Hom ` C )
10	1 6 7 8 9	thincmo	|- ( ph -> E* f f e. ( X ( Hom ` C ) Y ) )
11	5	oveqd	|- ( ph -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
12	11	eleq2d	|- ( ph -> ( f e. ( X H Y ) <-> f e. ( X ( Hom ` C ) Y ) ) )
13	12	mobidv	|- ( ph -> ( E* f f e. ( X H Y ) <-> E* f f e. ( X ( Hom ` C ) Y ) ) )
14	10 13	mpbird	|- ( ph -> E* f f e. ( X H Y ) )