Theorem slotsdifplendx2

Description: The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval . (Contributed by AV, 12-Nov-2024)

	Ref	Expression
Assertion	slotsdifplendx2	$$⊢\left({\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		10re	$$⊢10\in ℝ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		5nn	$$⊢5\in \mathbb{N}$$
5		5pos	$$⊢0<5$$
6	2 3 4 5	declt	$$⊢10<15$$
7	1 6	ltneii	$$⊢10\ne 15$$
8		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
9		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
10	8 9	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 15$$
11	7 10	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
12		4nn	$$⊢4\in \mathbb{N}$$
13		4pos	$$⊢0<4$$
14	2 3 12 13	declt	$$⊢10<14$$
15	1 14	ltneii	$$⊢10\ne 14$$
16		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
17	8 16	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 14$$
18	15 17	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
19	11 18	pm3.2i	$$⊢\left({\le }_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\right)$$