Metamath Proof Explorer

Theorem tsetndxnn

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

Ref Expression
Assertion tsetndxnn 
|- ( TopSet ` ndx ) e. NN

Proof

Step Hyp Ref Expression
1 tsetndx 
 |-  ( TopSet ` ndx ) = 9
2 9nn 
 |-  9 e. NN
3 1 2 eqeltri 
 |-  ( TopSet ` ndx ) e. NN