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 ) )