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} \neq \leq_{ndx} \land TopSet (ndx) \neq \leq_{ndx})$

Proof

Step	Hyp	Ref	Expression
1		4re	$⊢ 4 \in ℝ$
2		4lt10	$⊢ 4 < 10$
3	1 2	ltneii	$⊢ 4 \neq 10$
4		starvndx	$⊢ *_{ndx} = 4$
5		plendx	$⊢ \leq_{ndx} = 10$
6	4 5	neeq12i	$⊢ *_{ndx} \neq \leq_{ndx} \leftrightarrow 4 \neq 10$
7	3 6	mpbir	$⊢ *_{ndx} \neq \leq_{ndx}$
8		9re	$⊢ 9 \in ℝ$
9		9lt10	$⊢ 9 < 10$
10	8 9	ltneii	$⊢ 9 \neq 10$
11		tsetndx	$⊢ TopSet (ndx) = 9$
12	11 5	neeq12i	$⊢ TopSet (ndx) \neq \leq_{ndx} \leftrightarrow 9 \neq 10$
13	10 12	mpbir	$⊢ TopSet (ndx) \neq \leq_{ndx}$
14	7 13	pm3.2i	$⊢ (*_{ndx} \neq \leq_{ndx} \land TopSet (ndx) \neq \leq_{ndx})$