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 ) =/= ( .s ` ndx ) /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) )

Proof

Step Hyp Ref Expression
1 5re 
 |-  5 e. RR
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 e. RR
9 6lt9 
 |-  6 < 9
10 8 9 gtneii 
 |-  9 =/= 6
11 vscandx 
 |-  ( .s ` ndx ) = 6
12 4 11 neeq12i 
 |-  ( ( TopSet ` ndx ) =/= ( .s ` ndx ) <-> 9 =/= 6 )
13 10 12 mpbir 
 |-  ( TopSet ` ndx ) =/= ( .s ` ndx )
14 8re 
 |-  8 e. RR
15 8lt9 
 |-  8 < 9
16 14 15 gtneii 
 |-  9 =/= 8
17 ipndx 
 |-  ( .i ` ndx ) = 8
18 4 17 neeq12i 
 |-  ( ( TopSet ` ndx ) =/= ( .i ` ndx ) <-> 9 =/= 8 )
19 16 18 mpbir 
 |-  ( TopSet ` ndx ) =/= ( .i ` ndx )
20 7 13 19 3pm3.2i 
 |-  ( ( TopSet ` ndx ) =/= ( Scalar ` ndx ) /\ ( TopSet ` ndx ) =/= ( .s ` ndx ) /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) )