Theorem edgfndxnn

Description: The index value of the edge function extractor 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, 21-Sep-2020)

	Ref	Expression
Assertion	edgfndxnn	|- ( .ef ` ndx ) e. NN

Proof

Step	Hyp	Ref	Expression
1		df-edgf	|- .ef = Slot ; 1 8
2		1nn0	|- 1 e. NN0
3		8nn	|- 8 e. NN
4	2 3	decnncl	|- ; 1 8 e. NN
5	1 4	ndxarg	|- ( .ef ` ndx ) = ; 1 8
6	5 4	eqeltri	|- ( .ef ` ndx ) e. NN