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

Metamath Proof Explorer

Theorem slotstnscsi

Description: The slots Scalar , .s and .i are different from the slot TopSet . Formerly part of sralem and proofs using it. (Contributed by AV, 29-Oct-2024)

Ref Expression
Assertion slotstnscsi ⊢ TopSet ⁡ ndx ≠ Scalar ⁡ ndx ∧ TopSet ⁡ ndx ≠ ⋅ ndx ∧ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx

Proof

Step Hyp Ref Expression
1 5re ⊢ 5 ∈ ℝ
2 5lt9 ⊢ 5 < 9
3 1 2 gtneii ⊢ 9 ≠ 5
4 tsetndx ⊢ TopSet ⁡ ndx = 9
5 scandx ⊢ Scalar ⁡ ndx = 5
6 4 5 neeq12i ⊢ TopSet ⁡ ndx ≠ Scalar ⁡ ndx ↔ 9 ≠ 5
7 3 6 mpbir ⊢ TopSet ⁡ ndx ≠ Scalar ⁡ ndx
8 6re ⊢ 6 ∈ ℝ
9 6lt9 ⊢ 6 < 9
10 8 9 gtneii ⊢ 9 ≠ 6
11 vscandx ⊢ ⋅ ndx = 6
12 4 11 neeq12i ⊢ TopSet ⁡ ndx ≠ ⋅ ndx ↔ 9 ≠ 6
13 10 12 mpbir ⊢ TopSet ⁡ ndx ≠ ⋅ ndx
14 8re ⊢ 8 ∈ ℝ
15 8lt9 ⊢ 8 < 9
16 14 15 gtneii ⊢ 9 ≠ 8
17 ipndx ⊢ ⋅ 𝑖 ⁡ ndx = 8
18 4 17 neeq12i ⊢ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx ↔ 9 ≠ 8
19 16 18 mpbir ⊢ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
20 7 13 19 3pm3.2i ⊢ TopSet ⁡ ndx ≠ Scalar ⁡ ndx ∧ TopSet ⁡ ndx ≠ ⋅ ndx ∧ TopSet ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx