Metamath Proof Explorer


Theorem itvndx

Description: Index value of the Interval (segment) slot. Use ndxarg . (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion itvndx
|- ( Itv ` ndx ) = ; 1 6

Proof

Step Hyp Ref Expression
1 df-itv
 |-  Itv = Slot ; 1 6
2 1nn0
 |-  1 e. NN0
3 6nn
 |-  6 e. NN
4 2 3 decnncl
 |-  ; 1 6 e. NN
5 1 4 ndxarg
 |-  ( Itv ` ndx ) = ; 1 6