Theorem prstcprs

Description: The category is a preordered set. (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	prstcprs	$$⊢\phi \to C\in \mathrm{Proset}$$

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}}_K={\mathrm{Base}}_K$$
4	1 2 3	prstcbas	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_C$$
5		eqidd	$$⊢\phi \to {\le }_K={\le }_K$$
6	1 2 5	prstcleval	$$⊢\phi \to {\le }_K={\le }_C$$
7		fvex	Could not format ( ProsetToCat ` K ) e. _V : No typesetting found for |- ( ProsetToCat ` K ) e. _V with typecode |-
8	1 7	eqeltrdi	$$⊢\phi \to C\in \mathrm{V}$$
9	4 6 8	isprsd	$$⊢\phi \to \left(C\in \mathrm{Proset}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_K\forall z\in {\mathrm{Base}}_K\left(x{\le }_{K}x\wedge \left(\left(x{\le }_{K}y\wedge y{\le }_{K}z\right)\to x{\le }_{K}z\right)\right)\right)$$
10	3 5 2	isprsd	$$⊢\phi \to \left(K\in \mathrm{Proset}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_K\forall z\in {\mathrm{Base}}_K\left(x{\le }_{K}x\wedge \left(\left(x{\le }_{K}y\wedge y{\le }_{K}z\right)\to x{\le }_{K}z\right)\right)\right)$$
11	9 10	bitr4d	$$⊢\phi \to \left(C\in \mathrm{Proset}\leftrightarrow K\in \mathrm{Proset}\right)$$
12	2 11	mpbird	$$⊢\phi \to C\in \mathrm{Proset}$$