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	No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
	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	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		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)$$