Theorem prstcnid

Description: Components other than Hom and comp are unchanged. (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}$$
	prstcnid.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	prstcnid.no	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
	prstcnid.nh	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
Assertion	prstcnid	$$⊢\phi \to E\left(K\right)=E\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		prstcnid.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
4		prstcnid.no	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
5		prstcnid.nh	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
6	3 5	setsnid	$$⊢E\left(K\right)=E\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)$$
7	1 2 3 4	prstcnidlem	$$⊢\phi \to E\left(C\right)=E\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)$$
8	6 7	eqtr4id	$$⊢\phi \to E\left(K\right)=E\left(C\right)$$