Theorem postcpos

Description: The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	postc.c	No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
	postc.k	$$⊢\phi \to K\in \mathrm{Proset}$$
Assertion	postcpos	$$⊢\phi \to \left(K\in \mathrm{Poset}\leftrightarrow C\in \mathrm{Poset}\right)$$

Proof

Step	Hyp	Ref	Expression
1		postc.c	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2		postc.k	$$⊢\phi \to K\in \mathrm{Proset}$$
3	1 2	prstcprs	$$⊢\phi \to C\in \mathrm{Proset}$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	1 2 4	prstcbas	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_C$$
6		eqidd	$$⊢\phi \to {\le }_K={\le }_K$$
7	1 2 6	prstcle	$$⊢\phi \to \left(x{\le }_{K}y\leftrightarrow x{\le }_{C}y\right)$$
8	7	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to \left(x{\le }_{K}y\leftrightarrow x{\le }_{C}y\right)$$
9	2 3 4 5 8	pospropd	$$⊢\phi \to \left(K\in \mathrm{Poset}\leftrightarrow C\in \mathrm{Poset}\right)$$