Theorem prstchom2

Description: Hom-sets of the constructed category are dependent on the preorder.

Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat ( see prstchom2ALT ). However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 21-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
	prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
	prstchom.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
	prstchom.e	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
	prstchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
	prstchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
Assertion	prstchom2	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \exists !ff\in \left(XHY\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
2		prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
3		prstchom.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
4		prstchom.e	$$⊢\phi \to H=\mathrm{Hom}\left(C\right)$$
5		prstchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
6		prstchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
7	1 2 3 4 5 6	prstchom	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)$$
8	1 2	prstcthin	$$⊢\phi \to C\in \mathrm{ThinCat}$$
9		eqidd	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_C$$
10	8 5 6 9 4	thincn0eu	$$⊢\phi \to \left(XHY\ne \varnothing \leftrightarrow \exists !ff\in \left(XHY\right)\right)$$
11	7 10	bitrd	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \exists !ff\in \left(XHY\right)\right)$$