Metamath Proof Explorer

Theorem ndxarg

Description: Get the numeric argument from a defined structure component extractor such as df-base . (Contributed by Mario Carneiro, 6-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 ndxarg.1 ${⊢}{E}=\mathrm{Slot}{N}$
2 ndxarg.2 ${⊢}{N}\in ℕ$
3 df-ndx ${⊢}\mathrm{ndx}={\mathrm{I}↾}_{ℕ}$
4 nnex ${⊢}ℕ\in \mathrm{V}$
5 resiexg ${⊢}ℕ\in \mathrm{V}\to {\mathrm{I}↾}_{ℕ}\in \mathrm{V}$
6 4 5 ax-mp ${⊢}{\mathrm{I}↾}_{ℕ}\in \mathrm{V}$
7 3 6 eqeltri ${⊢}\mathrm{ndx}\in \mathrm{V}$
8 7 1 strfvn ${⊢}{E}\left(\mathrm{ndx}\right)=\mathrm{ndx}\left({N}\right)$
9 3 fveq1i ${⊢}\mathrm{ndx}\left({N}\right)=\left({\mathrm{I}↾}_{ℕ}\right)\left({N}\right)$
10 fvresi ${⊢}{N}\in ℕ\to \left({\mathrm{I}↾}_{ℕ}\right)\left({N}\right)={N}$
11 2 10 ax-mp ${⊢}\left({\mathrm{I}↾}_{ℕ}\right)\left({N}\right)={N}$
12 8 9 11 3eqtri ${⊢}{E}\left(\mathrm{ndx}\right)={N}$