Description: The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. Formerly part of proof for tuslem . (Contributed by AV, 28-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | basendxltunifndx | |- ( Base ` ndx ) < ( UnifSet ` ndx ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn | |- 1 e. NN |
|
| 2 | 3nn0 | |- 3 e. NN0 |
|
| 3 | 1nn0 | |- 1 e. NN0 |
|
| 4 | 1lt10 | |- 1 < ; 1 0 |
|
| 5 | 1 2 3 4 | declti | |- 1 < ; 1 3 |
| 6 | basendx | |- ( Base ` ndx ) = 1 |
|
| 7 | unifndx | |- ( UnifSet ` ndx ) = ; 1 3 |
|
| 8 | 5 6 7 | 3brtr4i | |- ( Base ` ndx ) < ( UnifSet ` ndx ) |