Theorem slotex 13096

Description: Existence of slot value. A corollary of slotslfn 13095. (Contributed by Jim Kingdon, 12-Feb-2023.)

Hypothesis

Ref	Expression
slotslfn.e	|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )

Assertion

Ref	Expression
slotex	|- ( A e. V -> ( E ` A ) e. _V )

Proof of Theorem slotex

Step	Hyp	Ref	Expression
1		slotslfn.e	. . 3 |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )
2	1	slotslfn 13095	. 2 |- E Fn _V
3		elex 2812	. 2 |- ( A e. V -> A e. _V )
4		funfvex 5650	. . 3 |- ( ( Fun E /\ A e. dom E ) -> ( E ` A ) e. _V )
5	4	funfni 5427	. 2 |- ( ( E Fn _V /\ A e. _V ) -> ( E ` A ) e. _V )
6	2, 3, 5	sylancr 414	1 |- ( A e. V -> ( E ` A ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395   e. wcel 2200   _Vcvv 2800   Fn wfn 5317   ` cfv 5322   NNcn 9131   ndxcnx 13066  Slot cslot 13068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295  ax-un 4526

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-br 4085  df-opab 4147  df-mpt 4148  df-id 4386  df-xp 4727  df-rel 4728  df-cnv 4729  df-co 4730  df-dm 4731  df-rn 4732  df-iota 5282  df-fun 5324  df-fn 5325  df-fv 5330  df-slot 13073

This theorem is referenced by:  topnfn  13314  topnvalg  13321  topnidg  13322  prdsplusgfval  13354  prdsmulrfval  13356  pwsval  13361  pwsbas  13362  pwsplusgval  13365  pwsmulrval  13366  imasex  13375  imasival  13376  imasbas  13377  imasplusg  13378  imasmulr  13379  imasaddfn  13387  imasaddval  13388  imasaddf  13389  imasmulfn  13390  imasmulval  13391  imasmulf  13392  qusaddval  13405  qusaddf  13406  qusmulval  13407  qusmulf  13408  xpsval  13422  ismgm  13427  plusfvalg  13433  plusffng  13435  gsumpropd2  13463  gsumsplit1r  13468  gsumprval  13469  issgrp  13473  ismnddef  13488  pwsmnd  13520  pws0g  13521  gsumfzz  13565  gsumwsubmcl  13566  gsumwmhm  13568  gsumfzcl  13569  grppropstrg  13589  grpsubval  13616  pwsgrp  13681  pwsinvg  13682  mulgval  13696  mulgfng  13698  mulgnngsum  13701  mulg1  13703  mulgnnp1  13704  mulgnndir  13725  subgintm  13772  isnsg  13776  gsumfzreidx  13911  gsumfzsubmcl  13912  gsumfzmptfidmadd  13913  gsumfzconst  13915  gsumfzmhm  13917  fnmgp  13922  mgpvalg  13923  mgpplusgg  13924  mgpex  13925  mgpbasg  13926  mgpscag  13927  mgptsetg  13928  mgpdsg  13930  mgpress  13931  isrng  13934  issrg  13965  isring  14000  opprvalg  14069  opprmulfvalg  14070  opprex  14073  opprsllem  14074  subrngintm  14213  islmod  14292  scaffvalg  14307  scafvalg  14308  scaffng  14310  rmodislmodlem  14351  rmodislmod  14352  lsssn0  14371  lss1d  14384  lssintclm  14385  ellspsn  14418  sraval  14438  sralemg  14439  srascag  14443  sravscag  14444  sraipg  14445  sraex  14447  crngridl  14531  znbaslemnn  14640  iedgvalg  15855  iedgex  15857  edgvalg  15897  edgstruct  15901