Theorem prstchom

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 . However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-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	prstchom	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \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	prstchomval	$$⊢\phi \to \underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(C\right)$$
8	4 7	eqtr4d	$$⊢\phi \to H=\underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}$$
9		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
11		1n0	$$⊢1_{𝑜}\ne \varnothing$$
12	11	a1i	$$⊢\phi \to 1_{𝑜}\ne \varnothing$$
13	8 10 12	ovconstbrn0d	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)$$