Theorem prstcle

Description: Value of the less-than-or-equal-to relation is 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}$$
	prstcle.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_K$$
Assertion	prstcle	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X{\le }_{C}Y\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		prstcle.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_K$$
4	1 2 3	prstcleval	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$
5	4	breqd	$$⊢\phi \to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X{\le }_{C}Y\right)$$