![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ndxarg | Structured version Visualization version GIF version |
Description: Get the numeric argument from a defined structure component extractor such as df-base 17081. (Contributed by Mario Carneiro, 6-Oct-2013.) |
Ref | Expression |
---|---|
ndxarg.e | ⊢ 𝐸 = Slot 𝑁 |
ndxarg.n | ⊢ 𝑁 ∈ ℕ |
Ref | Expression |
---|---|
ndxarg | ⊢ (𝐸‘ndx) = 𝑁 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ndx 17063 | . . . 4 ⊢ ndx = ( I ↾ ℕ) | |
2 | nnex 12156 | . . . . 5 ⊢ ℕ ∈ V | |
3 | resiexg 7848 | . . . . 5 ⊢ (ℕ ∈ V → ( I ↾ ℕ) ∈ V) | |
4 | 2, 3 | ax-mp 5 | . . . 4 ⊢ ( I ↾ ℕ) ∈ V |
5 | 1, 4 | eqeltri 2834 | . . 3 ⊢ ndx ∈ V |
6 | ndxarg.e | . . 3 ⊢ 𝐸 = Slot 𝑁 | |
7 | 5, 6 | strfvn 17055 | . 2 ⊢ (𝐸‘ndx) = (ndx‘𝑁) |
8 | 1 | fveq1i 6841 | . 2 ⊢ (ndx‘𝑁) = (( I ↾ ℕ)‘𝑁) |
9 | ndxarg.n | . . 3 ⊢ 𝑁 ∈ ℕ | |
10 | fvresi 7116 | . . 3 ⊢ (𝑁 ∈ ℕ → (( I ↾ ℕ)‘𝑁) = 𝑁) | |
11 | 9, 10 | ax-mp 5 | . 2 ⊢ (( I ↾ ℕ)‘𝑁) = 𝑁 |
12 | 7, 8, 11 | 3eqtri 2768 | 1 ⊢ (𝐸‘ndx) = 𝑁 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 Vcvv 3444 I cid 5529 ↾ cres 5634 ‘cfv 6494 ℕcn 12150 Slot cslot 17050 ndxcnx 17062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 ax-cnex 11104 ax-1cn 11106 ax-addcl 11108 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5530 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5587 df-we 5589 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6252 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-ov 7357 df-om 7800 df-2nd 7919 df-frecs 8209 df-wrecs 8240 df-recs 8314 df-rdg 8353 df-nn 12151 df-slot 17051 df-ndx 17063 |
This theorem is referenced by: ndxid 17066 basendx 17089 basendxnnOLD 17091 2strstr 17102 2strstr1OLD 17106 2strop1 17108 resslemOLD 17120 plusgndx 17156 basendxnplusgndxOLD 17161 mulrndx 17171 basendxnmulrndxOLD 17174 starvndx 17180 scandx 17192 vscandx 17197 ipndx 17208 tsetndx 17230 plendx 17244 ocndx 17259 dsndx 17263 unifndx 17273 homndx 17289 ccondx 17291 slotsbhcdifOLD 17294 oppglemOLD 19125 symgvalstructOLD 19175 mgplemOLD 19897 opprlemOLD 20051 rmodislmodOLD 20387 sralemOLD 20635 zlmlemOLD 20914 znbaslemOLD 20938 opsrbaslemOLD 21447 tnglemOLD 23993 itvndx 27277 lngndx 27278 ttglemOLD 27718 cchhllemOLD 27734 edgfndx 27838 baseltedgfOLD 27843 resvlemOLD 32018 hlhilslemOLD 40391 mnringnmulrdOLD 42470 |
Copyright terms: Public domain | W3C validator |