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 )