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) (Proof shortened by AV, 28-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 basendx
 |-  ( Base ` ndx ) = 1
2 1re
 |-  1 e. RR
3 1lt3
 |-  1 < 3
4 2 3 ltneii
 |-  1 =/= 3
5 mulrndx
 |-  ( .r ` ndx ) = 3
6 4 5 neeqtrri
 |-  1 =/= ( .r ` ndx )
7 1 6 eqnetri
 |-  ( Base ` ndx ) =/= ( .r ` ndx )