Theorem slotsdifplendx

Description: The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfun . (Contributed by AV, 11-Nov-2024)

	Ref	Expression
Assertion	slotsdifplendx	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) )

Proof

Step	Hyp	Ref	Expression
1		4re	⊢ 4 ∈ ℝ
2		4lt10	⊢ 4 < ; 1 0
3	1 2	ltneii	⊢ 4 ≠ ; 1 0
4		starvndx	⊢ ( *𝑟 ‘ ndx ) = 4
5		plendx	⊢ ( le ‘ ndx ) = ; 1 0
6	4 5	neeq12i	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ↔ 4 ≠ ; 1 0 )
7	3 6	mpbir	⊢ ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx )
8		9re	⊢ 9 ∈ ℝ
9		9lt10	⊢ 9 < ; 1 0
10	8 9	ltneii	⊢ 9 ≠ ; 1 0
11		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
12	11 5	neeq12i	⊢ ( ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) ↔ 9 ≠ ; 1 0 )
13	10 12	mpbir	⊢ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx )
14	7 13	pm3.2i	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) )