ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ndxarg GIF version

Theorem ndxarg 11818
Description: Get the numeric argument from a defined structure component extractor such as df-base 11801. (Contributed by Mario Carneiro, 6-Oct-2013.)
Hypotheses
Ref Expression
ndxarg.1 𝐸 = Slot 𝑁
ndxarg.2 𝑁 ∈ ℕ
Assertion
Ref Expression
ndxarg (𝐸‘ndx) = 𝑁

Proof of Theorem ndxarg
StepHypRef Expression
1 df-ndx 11798 . . . 4 ndx = ( I ↾ ℕ)
2 nnex 8629 . . . . 5 ℕ ∈ V
3 resiexg 4820 . . . . 5 (ℕ ∈ V → ( I ↾ ℕ) ∈ V)
42, 3ax-mp 7 . . . 4 ( I ↾ ℕ) ∈ V
51, 4eqeltri 2185 . . 3 ndx ∈ V
6 ndxarg.1 . . 3 𝐸 = Slot 𝑁
7 ndxarg.2 . . 3 𝑁 ∈ ℕ
85, 6, 7strnfvn 11816 . 2 (𝐸‘ndx) = (ndx‘𝑁)
91fveq1i 5374 . 2 (ndx‘𝑁) = (( I ↾ ℕ)‘𝑁)
10 fvresi 5565 . . 3 (𝑁 ∈ ℕ → (( I ↾ ℕ)‘𝑁) = 𝑁)
117, 10ax-mp 7 . 2 (( I ↾ ℕ)‘𝑁) = 𝑁
128, 9, 113eqtri 2137 1 (𝐸‘ndx) = 𝑁
Colors of variables: wff set class
Syntax hints:   = wceq 1312  wcel 1461  Vcvv 2655   I cid 4168  cres 4499  cfv 5079  cn 8623  ndxcnx 11792  Slot cslot 11794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-cnex 7629  ax-resscn 7630  ax-1re 7632  ax-addrcl 7635
This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-sbc 2877  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-br 3894  df-opab 3948  df-mpt 3949  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-iota 5044  df-fun 5081  df-fv 5087  df-inn 8624  df-ndx 11798  df-slot 11799
This theorem is referenced by:  ndxid  11819  ndxslid  11820  strndxid  11823  basendx  11849  basendxnn  11850  plusgndx  11888  2strstrg  11895  2strbasg  11896  2stropg  11897  2strstr1g  11898  2strop1g  11900  basendxnplusgndx  11901  mulrndx  11905  basendxnmulrndx  11909  starvndx  11914  scandx  11922  vscandx  11925  ipndx  11933  tsetndx  11943  plendx  11950  dsndx  11953
  Copyright terms: Public domain W3C validator