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 ∈ ℕ
3 1 2 ndxarg ( Base ‘ ndx ) = 1
4 1re 1 ∈ ℝ
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 )