Theorem plendxnn

Description: The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024)

	Ref	Expression
Assertion	plendxnn	|- ( le ` ndx ) e. NN

Proof

Step	Hyp	Ref	Expression
1		plendx	|- ( le ` ndx ) = ; 1 0
2		10nn	|- ; 1 0 e. NN
3	1 2	eqeltri	|- ( le ` ndx ) e. NN