Theorem prstchomval

Description: Hom-sets of the constructed category which depend on an arbitrary definition. (Contributed by Zhi Wang, 20-Sep-2024) (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}$$
	prstchomval.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
Assertion	prstchomval	$$⊢\phi \to \underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(C\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		prstchomval.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
4		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
5		slotsbhcdif	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
6	5	simp3i	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
7	1 2 4 6	prstcnidlem	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)$$
8		fvex	$$⊢{\le }_K\in \mathrm{V}$$
9		snex	$$⊢\left\{1_{𝑜}\right\}\in \mathrm{V}$$
10	8 9	xpex	$$⊢{\le }_K\times \left\{1_{𝑜}\right\}\in \mathrm{V}$$
11	4	setsid	$$⊢\left(K\in \mathrm{Proset}\wedge {\le }_K\times \left\{1_{𝑜}\right\}\in \mathrm{V}\right)\to {\le }_K\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)$$
12	2 10 11	sylancl	$$⊢\phi \to {\le }_K\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)$$
13		eqidd	$$⊢\phi \to {\le }_K={\le }_K$$
14	1 2 13	prstcleval	$$⊢\phi \to {\le }_K={\le }_C$$
15	14 3	eqtr4d	$$⊢\phi \to {\le }_K=\underset{\dot{}}{\le }$$
16	15	xpeq1d	$$⊢\phi \to {\le }_K\times \left\{1_{𝑜}\right\}=\underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}$$
17	7 12 16	3eqtr2rd	$$⊢\phi \to \underset{\dot{}}{\le }\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(C\right)$$