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 TopSetndxScalarndxTopSetndxndxTopSetndx𝑖ndx

Proof

Step Hyp Ref Expression
1 5re 5
2 5lt9 5<9
3 1 2 gtneii 95
4 tsetndx TopSetndx=9
5 scandx Scalarndx=5
6 4 5 neeq12i TopSetndxScalarndx95
7 3 6 mpbir TopSetndxScalarndx
8 6re 6
9 6lt9 6<9
10 8 9 gtneii 96
11 vscandx ndx=6
12 4 11 neeq12i TopSetndxndx96
13 10 12 mpbir TopSetndxndx
14 8re 8
15 8lt9 8<9
16 14 15 gtneii 98
17 ipndx 𝑖ndx=8
18 4 17 neeq12i TopSetndx𝑖ndx98
19 16 18 mpbir TopSetndx𝑖ndx
20 7 13 19 3pm3.2i TopSetndxScalarndxTopSetndxndxTopSetndx𝑖ndx