Theorem slotex 13256

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

Hypothesis

Ref	Expression
slotslfn.e	⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)

Assertion

Ref	Expression
slotex	⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V)

Proof of Theorem slotex

Step	Hyp	Ref	Expression
1		slotslfn.e	. . 3 ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)
2	1	slotslfn 13255	. 2 ⊢ 𝐸 Fn V
3		elex 2827	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		funfvex 5689	. . 3 ⊢ ((Fun 𝐸 ∧ 𝐴 ∈ dom 𝐸) → (𝐸‘𝐴) ∈ V)
5	4	funfni 5460	. 2 ⊢ ((𝐸 Fn V ∧ 𝐴 ∈ V) → (𝐸‘𝐴) ∈ V)
6	2, 3, 5	sylancr 414	1 ⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  Vcvv 2815   Fn wfn 5349  ‘cfv 5354  ℕcn 9239  ndxcnx 13226  Slot cslot 13228

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-iota 5314  df-fun 5356  df-fn 5357  df-fv 5362  df-slot 13233

This theorem is referenced by:  topnfn  13474  topnvalg  13481  topnidg  13482  prdsplusgfval  13514  prdsmulrfval  13516  pwsval  13521  pwsbas  13522  pwsplusgval  13525  pwsmulrval  13526  imasex  13535  imasival  13536  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfn  13547  imasaddval  13548  imasaddf  13549  imasmulfn  13550  imasmulval  13551  imasmulf  13552  qusaddval  13565  qusaddf  13566  qusmulval  13567  qusmulf  13568  xpsval  13582  ismgm  13587  plusfvalg  13593  plusffng  13595  gsumpropd2  13623  gsumsplit1r  13628  gsumprval  13629  issgrp  13633  ismnddef  13648  pwsmnd  13680  pws0g  13681  gsumfzz  13725  gsumwsubmcl  13726  gsumwmhm  13728  gsumfzcl  13729  grppropstrg  13749  grpsubval  13776  pwsgrp  13841  pwsinvg  13842  mulgval  13856  mulgfng  13858  mulgnngsum  13861  mulg1  13863  mulgnnp1  13864  mulgnndir  13885  subgintm  13932  isnsg  13936  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzconst  14075  gsumfzmhm  14077  fnmgp  14083  mgpvalg  14084  mgpplusgg  14085  mgpex  14086  mgpbasg  14087  mgpscag  14088  mgptsetg  14089  mgpdsg  14091  mgpress  14092  isrng  14095  issrg  14126  isring  14161  opprvalg  14230  opprmulfvalg  14231  opprex  14234  opprsllem  14235  subrngintm  14374  islmod  14456  scaffvalg  14471  scafvalg  14472  scaffng  14474  rmodislmodlem  14515  rmodislmod  14516  lsssn0  14535  lss1d  14548  lssintclm  14549  ellspsn  14582  sraval  14602  sralemg  14603  srascag  14607  sravscag  14608  sraipg  14609  sraex  14611  crngridl  14695  znbaslemnn  14804  iedgvalg  16029  iedgex  16031  edgvalg  16071  edgstruct  16076  gfsumval  16879  gsumgfsumlem  16882