Theorem basendxnn

Description: The index value of the base set 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, 23-Sep-2020)

	Ref	Expression
Assertion	basendxnn	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
2		1nn	$$⊢1\in \mathbb{N}$$
3	1 2	ndxarg	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4	3 2	eqeltri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathbb{N}$$