Theorem prstchom2ALT

Description: Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc . See prstchom2 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	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)$$
Assertion	prstchom2ALT	$$⊢\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		ovex	$$⊢XHY\in \mathrm{V}$$
6	1 2 3	prstchomval	$$⊢\phi \to \underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(C\right)$$
7	4 6	eqtr4d	$$⊢\phi \to H=\underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}$$
8		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
10		1n0	$$⊢1_{𝑜}\ne \varnothing$$
11	10	a1i	$$⊢\phi \to 1_{𝑜}\ne \varnothing$$
12	7 9 11	ovconstbrd	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY=1_{𝑜}\right)$$
13	12	biimpa	$$⊢\left(\phi \wedge X\underset{\dot{}}{\le }Y\right)\to XHY=1_{𝑜}$$
14		eqeng	$$⊢XHY\in \mathrm{V}\to \left(XHY=1_{𝑜}\to \left(XHY\right)\approx 1_{𝑜}\right)$$
15	5 13 14	mpsyl	$$⊢\left(\phi \wedge X\underset{\dot{}}{\le }Y\right)\to \left(XHY\right)\approx 1_{𝑜}$$
16		euen1b	$$⊢\left(XHY\right)\approx 1_{𝑜}\leftrightarrow \exists !ff\in \left(XHY\right)$$
17	15 16	sylib	$$⊢\left(\phi \wedge X\underset{\dot{}}{\le }Y\right)\to \exists !ff\in \left(XHY\right)$$
18		euex	$$⊢\exists !ff\in \left(XHY\right)\to \exists ff\in \left(XHY\right)$$
19		n0	$$⊢XHY\ne \varnothing \leftrightarrow \exists ff\in \left(XHY\right)$$
20	18 19	sylibr	$$⊢\exists !ff\in \left(XHY\right)\to XHY\ne \varnothing$$
21	7 9 11	ovconstbrn0d	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow XHY\ne \varnothing \right)$$
22	21	biimpar	$$⊢\left(\phi \wedge XHY\ne \varnothing \right)\to X\underset{\dot{}}{\le }Y$$
23	20 22	sylan2	$$⊢\left(\phi \wedge \exists !ff\in \left(XHY\right)\right)\to X\underset{\dot{}}{\le }Y$$
24	17 23	impbida	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \exists !ff\in \left(XHY\right)\right)$$