Metamath Proof Explorer


Theorem basendxnplusgndx

Description: The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 17-Oct-2024)

Ref Expression
Assertion basendxnplusgndx
|- ( Base ` ndx ) =/= ( +g ` ndx )

Proof

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