Metamath Proof Explorer


Theorem basendxnmulrndx

Description: The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020)

Ref Expression
Assertion basendxnmulrndx
|- ( Base ` ndx ) =/= ( .r ` ndx )

Proof

Step Hyp Ref Expression
1 df-base
 |-  Base = Slot 1
2 1nn
 |-  1 e. NN
3 1 2 ndxarg
 |-  ( Base ` ndx ) = 1
4 1re
 |-  1 e. RR
5 1lt3
 |-  1 < 3
6 4 5 ltneii
 |-  1 =/= 3
7 mulrndx
 |-  ( .r ` ndx ) = 3
8 6 7 neeqtrri
 |-  1 =/= ( .r ` ndx )
9 3 8 eqnetri
 |-  ( Base ` ndx ) =/= ( .r ` ndx )