Theorem ndxid

Description: A structure component extractor is defined by its own index. This theorem, together with strfv below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base and the ; 1 0 in df-ple , making it easier to change should the need arise.

For example, we can refer to a specific poset with base set B and order relation L using { <. ( Basendx ) , B >. , <. ( lendx ) , L >. } rather than { <. 1 , B >. , <. ; 1 0 , L >. } . The latter, while shorter to state, requires revision if we later change ; 1 0 to some other number, and it may also be harder to remember. (Contributed by NM, 19-Oct-2012) (Revised by Mario Carneiro, 6-Oct-2013) (Proof shortened by BJ, 27-Dec-2021)

	Ref	Expression
Hypotheses	ndxarg.1	$$⊢E=\mathrm{Slot}N$$
	ndxarg.2	$$⊢N\in \mathbb{N}$$
Assertion	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ndxarg.1	$$⊢E=\mathrm{Slot}N$$
2		ndxarg.2	$$⊢N\in \mathbb{N}$$
3	1 2	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
4	3	eqcomi	$$⊢N=E\left(\mathrm{ndx}\right)$$
5		sloteq	$$⊢N=E\left(\mathrm{ndx}\right)\to \mathrm{Slot}N=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
6	1 5	syl5eq	$$⊢N=E\left(\mathrm{ndx}\right)\to E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
7	4 6	ax-mp	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$