Theorem prstcleval

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	prstcleval	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$

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		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
5		10re	$$⊢10\in ℝ$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8		5nn	$$⊢5\in \mathbb{N}$$
9	8	nngt0i	$$⊢0<5$$
10	6 7 8 9	declt	$$⊢10<15$$
11	5 10	ltneii	$$⊢10\ne 15$$
12		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
13		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
14	12 13	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 15$$
15	11 14	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
16		4nn	$$⊢4\in \mathbb{N}$$
17	16	nngt0i	$$⊢0<4$$
18	6 7 16 17	declt	$$⊢10<14$$
19	5 18	ltneii	$$⊢10\ne 14$$
20		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
21	12 20	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 14$$
22	19 21	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
23	1 2 4 15 22	prstcnid	$$⊢\phi \to {\le }_K={\le }_C$$
24	3 23	eqtrd	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_C$$