This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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) (Proof shortened by AV, 13-Oct-2024)

		Ref	Expression
	Assertion	edgfndxnn	$⊢ ef (ndx) \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		edgfndx	$⊢ ef (ndx) = 18$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		8nn	$⊢ 8 \in ℕ$
4	2 3	decnncl	$⊢ 18 \in ℕ$
5	1 4	eqeltri	$⊢ ef (ndx) \in ℕ$