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 |
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 |