Theorem ndxarg 16556

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

Hypotheses

Ref	Expression
ndxarg.1	⊢ 𝐸 = Slot 𝑁
ndxarg.2	⊢ 𝑁 ∈ ℕ

Assertion

Ref	Expression
ndxarg	⊢ (𝐸‘ndx) = 𝑁

Proof of Theorem ndxarg

Step	Hyp	Ref	Expression
1		df-ndx 16534	. . . 4 ⊢ ndx = ( I ↾ ℕ)
2		nnex 11670	. . . . 5 ⊢ ℕ ∈ V
3		resiexg 7622	. . . . 5 ⊢ (ℕ ∈ V → ( I ↾ ℕ) ∈ V)
4	2, 3	ax-mp 5	. . . 4 ⊢ ( I ↾ ℕ) ∈ V
5	1, 4	eqeltri 2849	. . 3 ⊢ ndx ∈ V
6		ndxarg.1	. . 3 ⊢ 𝐸 = Slot 𝑁
7	5, 6	strfvn 16553	. 2 ⊢ (𝐸‘ndx) = (ndx‘𝑁)
8	1	fveq1i 6657	. 2 ⊢ (ndx‘𝑁) = (( I ↾ ℕ)‘𝑁)
9		ndxarg.2	. . 3 ⊢ 𝑁 ∈ ℕ
10		fvresi 6924	. . 3 ⊢ (𝑁 ∈ ℕ → (( I ↾ ℕ)‘𝑁) = 𝑁)
11	9, 10	ax-mp 5	. 2 ⊢ (( I ↾ ℕ)‘𝑁) = 𝑁
12	7, 8, 11	3eqtri 2786	1 ⊢ (𝐸‘ndx) = 𝑁

Syntax hints:   = wceq 1539   ∈ wcel 2112  Vcvv 3410   I cid 5427   ↾ cres 5524  ‘cfv 6333  ℕcn 11664  ndxcnx 16528  Slot cslot 16530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-1cn 10623  ax-addcl 10625

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7151  df-om 7578  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-nn 11665  df-ndx 16534  df-slot 16535

This theorem is referenced by:  ndxid  16557  basendx  16595  basendxnn  16596  resslem  16605  plusgndx  16643  2strstr  16650  2strstr1  16653  2strop1  16655  basendxnplusgndx  16656  mulrndx  16663  basendxnmulrndx  16666  starvndx  16671  scandx  16680  vscandx  16682  ipndx  16689  tsetndx  16707  plendx  16714  ocndx  16721  dsndx  16723  unifndx  16725  homndx  16735  ccondx  16737  slotsbhcdif  16741  oppglem  18535  symgvalstruct  18582  mgplem  19302  opprlem  19439  rmodislmod  19760  sralem  20007  zlmlem  20276  znbaslem  20296  opsrbaslem  20799  tnglem  23332  itvndx  26323  lngndx  26324  ttglem  26759  cchhllem  26770  edgfndxnn  26874  baseltedgf  26876  resvlem  31046  hlhilslem  39504  mnringnmulrd  41285