Metamath Proof Explorer


Theorem unifndxnn

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 UnifSetndx

Proof

Step Hyp Ref Expression
1 unifndx UnifSetndx=13
2 1nn0 10
3 3nn 3
4 2 3 decnncl 13
5 1 4 eqeltri UnifSetndx