This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem slotsdifplendx

Description: The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT . (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 ) )