Theorem prstcval

Description: Lemma for prstcnidlem and prstcthin . (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	prstcnid.c	No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
	prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
Assertion	prstcval	$$⊢\phi \to C=\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩$$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2		prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
3		id	$$⊢k=K\to k=K$$
4		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
5	4	xpeq1d	$$⊢k=K\to {\le }_k\times \left\{1_{𝑜}\right\}={\le }_K\times \left\{1_{𝑜}\right\}$$
6	5	opeq2d	$$⊢k=K\to ⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩=⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩$$
7	3 6	oveq12d	$$⊢k=K\to k\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩=K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩$$
8	7	oveq1d	$$⊢k=K\to \left(k\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩=\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩$$
9		df-prstc	Could not format ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
10		ovex	$$⊢\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩\in \mathrm{V}$$
11	8 9 10	fvmpt	Could not format ( K e. Proset -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ( K e. Proset -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
12	2 11	syl	Could not format ( ph -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for |- ( ph -> ( ProsetToCat ` K ) = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-
13	1 12	eqtrd	$$⊢\phi \to C=\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩$$