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	No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
	thincmo.x	$$⊢\phi \to X\in B$$
	thincmo.y	$$⊢\phi \to Y\in B$$
	thincn0eu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
	thincn0eu.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
Assertion	thincmod	$$⊢\phi \to {\exists }^{*}ff\in \left(XHY\right)$$

Proof

Step	Hyp	Ref	Expression
1		thincmo.c	Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2		thincmo.x	$$⊢\phi \to X\in B$$
3		thincmo.y	$$⊢\phi \to Y\in B$$
4		thincn0eu.b	$$⊢\phi \to B={\mathrm{Base}}_C$$
5		thincn0eu.h	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
6	2 4	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
7	3 4	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
10	1 6 7 8 9	thincmo	$$⊢\phi \to {\exists }^{*}ff\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
11	5	oveqd	$$⊢\phi \to XHY=X\mathrm{Hom}\left(C\right)Y$$
12	11	eleq2d	$$⊢\phi \to \left(f\in \left(XHY\right)\leftrightarrow f\in \left(X\mathrm{Hom}\left(C\right)Y\right)\right)$$
13	12	mobidv	$$⊢\phi \to \left({\exists }^{*}ff\in \left(XHY\right)\leftrightarrow {\exists }^{*}ff\in \left(X\mathrm{Hom}\left(C\right)Y\right)\right)$$
14	10 13	mpbird	$$⊢\phi \to {\exists }^{*}ff\in \left(XHY\right)$$