Metamath Proof Explorer

Theorem slotsbaseefdif

Description: The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion slotsbaseefdif 
|- ( Base ` ndx ) =/= ( .ef ` ndx )

Proof

Step Hyp Ref Expression
1 basendxnn 
 |-  ( Base ` ndx ) e. NN
2 1 nnrei 
 |-  ( Base ` ndx ) e. RR
3 baseltedgf 
 |-  ( Base ` ndx ) < ( .ef ` ndx )
4 2 3 ltneii 
 |-  ( Base ` ndx ) =/= ( .ef ` ndx )