Theorem slotex 12539

Description: Existence of slot value. A corollary of slotslfn 12538. (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 12538	. 2 ⊢ 𝐸 Fn V
3		elex 2763	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		funfvex 5551	. . 3 ⊢ ((Fun 𝐸 ∧ 𝐴 ∈ dom 𝐸) → (𝐸‘𝐴) ∈ V)
5	4	funfni 5335	. 2 ⊢ ((𝐸 Fn V ∧ 𝐴 ∈ V) → (𝐸‘𝐴) ∈ V)
6	2, 3, 5	sylancr 414	1 ⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2160  Vcvv 2752   Fn wfn 5230  ‘cfv 5235  ℕcn 8949  ndxcnx 12509  Slot cslot 12511

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-iota 5196  df-fun 5237  df-fn 5238  df-fv 5243  df-slot 12516

This theorem is referenced by:  topnfn  12749  topnvalg  12756  topnidg  12757  imasex  12782  imasival  12783  imasbas  12784  imasplusg  12785  imasmulr  12786  imasaddfn  12794  imasaddval  12795  imasaddf  12796  imasmulfn  12797  imasmulval  12798  imasmulf  12799  qusaddval  12811  qusaddf  12812  qusmulval  12813  qusmulf  12814  xpsval  12828  ismgm  12833  plusfvalg  12839  plusffng  12841  issgrp  12866  ismnddef  12879  grppropstrg  12964  grpsubval  12990  mulgval  13064  mulgfng  13066  mulg1  13069  mulgnnp1  13070  mulgnndir  13091  subgintm  13137  isnsg  13141  fnmgp  13276  mgpvalg  13277  mgpplusgg  13278  mgpex  13279  mgpbasg  13280  mgpscag  13281  mgptsetg  13282  mgpdsg  13284  mgpress  13285  isrng  13288  issrg  13319  isring  13354  opprvalg  13419  opprmulfvalg  13420  opprex  13423  opprsllem  13424  subrngintm  13559  islmod  13607  scaffvalg  13622  scafvalg  13623  scaffng  13625  rmodislmodlem  13666  rmodislmod  13667  lsssn0  13686  lss1d  13699  lssintclm  13700  lspsnel  13733  sraval  13753  sralemg  13754  srascag  13758  sravscag  13759  sraipg  13760  sraex  13762  crngridl  13844  znbaslemnn  13935