Metamath Proof Explorer

Theorem plusgndxnn

Description: The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024)

Ref Expression
Assertion plusgndxnn 
|- ( +g ` ndx ) e. NN

Proof

Step Hyp Ref Expression
1 plusgndx 
 |-  ( +g ` ndx ) = 2
2 2nn 
 |-  2 e. NN
3 1 2 eqeltri 
 |-  ( +g ` ndx ) e. NN