Description: The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem . (Contributed by AV, 28-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | unifndxnn | |- ( UnifSet ` ndx ) e. NN |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unifndx | |- ( UnifSet ` ndx ) = ; 1 3 |
|
| 2 | 1nn0 | |- 1 e. NN0 |
|
| 3 | 3nn | |- 3 e. NN |
|
| 4 | 2 3 | decnncl | |- ; 1 3 e. NN |
| 5 | 1 4 | eqeltri | |- ( UnifSet ` ndx ) e. NN |