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)

Ref Expression
Assertion basendxnplusgndx
|- ( Base ` ndx ) =/= ( +g ` 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 1ne2
 |-  1 =/= 2
5 plusgndx
 |-  ( +g ` ndx ) = 2
6 4 5 neeqtrri
 |-  1 =/= ( +g ` ndx )
7 3 6 eqnetri
 |-  ( Base ` ndx ) =/= ( +g ` ndx )