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	⊢ 𝐸 = Slot 𝑁
	ndxarg.2	⊢ 𝑁 ∈ ℕ
Assertion	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		ndxarg.1	⊢ 𝐸 = Slot 𝑁
2		ndxarg.2	⊢ 𝑁 ∈ ℕ
3	1 2	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
4	3	eqcomi	⊢ 𝑁 = ( 𝐸 ‘ ndx )
5		sloteq	⊢ ( 𝑁 = ( 𝐸 ‘ ndx ) → Slot 𝑁 = Slot ( 𝐸 ‘ ndx ) )
6	1 5	syl5eq	⊢ ( 𝑁 = ( 𝐸 ‘ ndx ) → 𝐸 = Slot ( 𝐸 ‘ ndx ) )
7	4 6	ax-mp	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )