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

Metamath Proof Explorer

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	$⊢ \leq_{ndx} \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		plendx	$⊢ \leq_{ndx} = 10$
2		10nn	$⊢ 10 \in ℕ$
3	1 2	eqeltri	$⊢ \leq_{ndx} \in ℕ$