Theorem prstcthin

Description: The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Hypotheses	prstcnid.c	No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
	prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
Assertion	prstcthin	Could not format assertion : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-

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		eqidd	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_C$$
4		eqidd	$$⊢\phi \to {\le }_C={\le }_C$$
5	1 2 4	prstchomval	$$⊢\phi \to {\le }_C\times \left\{1_{𝑜}\right\}=\mathrm{Hom}\left(C\right)$$
6		ovex	$$⊢K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\in \mathrm{V}$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8		ccoid	$$⊢\mathrm{comp}=\mathrm{Slot}\mathrm{comp}\left(\mathrm{ndx}\right)$$
9	8	setsid	$$⊢\left(K\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_K\times \left\{1_{𝑜}\right\}⟩\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to \varnothing =\mathrm{comp}\left(\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 ⟩\right)$$
10	6 7 9	mp2an	$$⊢\varnothing =\mathrm{comp}\left(\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 ⟩\right)$$
11	1 2	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 ⟩$$
12	11	fveq2d	$$⊢\phi \to \mathrm{comp}\left(C\right)=\mathrm{comp}\left(\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 ⟩\right)$$
13	10 12	eqtr4id	$$⊢\phi \to \varnothing =\mathrm{comp}\left(C\right)$$
14	1 2	prstcprs	$$⊢\phi \to C\in \mathrm{Proset}$$
15	3 5 13 4 14	prsthinc	Could not format ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) ) : No typesetting found for |- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) ) with typecode |-
16	15	simpld	Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-