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

Theorem setsslid 12515
Description: Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
Hypothesis
Ref Expression
setsslid.e (𝐸 = Slot (πΈβ€˜ndx) ∧ (πΈβ€˜ndx) ∈ β„•)
Assertion
Ref Expression
setsslid ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 = (πΈβ€˜(π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩)))

Proof of Theorem setsslid
StepHypRef Expression
1 setsslid.e . . . . 5 (𝐸 = Slot (πΈβ€˜ndx) ∧ (πΈβ€˜ndx) ∈ β„•)
21simpri 113 . . . 4 (πΈβ€˜ndx) ∈ β„•
3 setsvala 12495 . . . 4 ((π‘Š ∈ 𝐴 ∧ (πΈβ€˜ndx) ∈ β„• ∧ 𝐢 ∈ 𝑉) β†’ (π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩) = ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
42, 3mp3an2 1325 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩) = ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
54fveq2d 5521 . 2 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (πΈβ€˜(π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩)) = (πΈβ€˜((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})))
61simpli 111 . . 3 𝐸 = Slot (πΈβ€˜ndx)
7 resexg 4949 . . . 4 (π‘Š ∈ 𝐴 β†’ (π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) ∈ V)
8 simpr 110 . . . . . 6 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 ∈ 𝑉)
9 opexg 4230 . . . . . 6 (((πΈβ€˜ndx) ∈ β„• ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V)
102, 8, 9sylancr 414 . . . . 5 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V)
11 snexg 4186 . . . . 5 (⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V β†’ {⟨(πΈβ€˜ndx), 𝐢⟩} ∈ V)
1210, 11syl 14 . . . 4 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ {⟨(πΈβ€˜ndx), 𝐢⟩} ∈ V)
13 unexg 4445 . . . 4 (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) ∈ V ∧ {⟨(πΈβ€˜ndx), 𝐢⟩} ∈ V) β†’ ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) ∈ V)
147, 12, 13syl2an2r 595 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) ∈ V)
152a1i 9 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (πΈβ€˜ndx) ∈ β„•)
166, 14, 15strnfvnd 12484 . 2 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (πΈβ€˜((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)))
17 snidg 3623 . . . . 5 ((πΈβ€˜ndx) ∈ β„• β†’ (πΈβ€˜ndx) ∈ {(πΈβ€˜ndx)})
18 fvres 5541 . . . . 5 ((πΈβ€˜ndx) ∈ {(πΈβ€˜ndx)} β†’ ((((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)})β€˜(πΈβ€˜ndx)) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)))
192, 17, 18mp2b 8 . . . 4 ((((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)})β€˜(πΈβ€˜ndx)) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx))
20 resres 4921 . . . . . . . . 9 ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}))
21 incom 3329 . . . . . . . . . . . 12 ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}) = ({(πΈβ€˜ndx)} ∩ (V βˆ– {(πΈβ€˜ndx)}))
22 disjdif 3497 . . . . . . . . . . . 12 ({(πΈβ€˜ndx)} ∩ (V βˆ– {(πΈβ€˜ndx)})) = βˆ…
2321, 22eqtri 2198 . . . . . . . . . . 11 ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}) = βˆ…
2423reseq2i 4906 . . . . . . . . . 10 (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)})) = (π‘Š β†Ύ βˆ…)
25 res0 4913 . . . . . . . . . 10 (π‘Š β†Ύ βˆ…) = βˆ…
2624, 25eqtri 2198 . . . . . . . . 9 (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)})) = βˆ…
2720, 26eqtri 2198 . . . . . . . 8 ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = βˆ…
2827a1i 9 . . . . . . 7 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = βˆ…)
292elexi 2751 . . . . . . . . . 10 (πΈβ€˜ndx) ∈ V
308elexd 2752 . . . . . . . . . 10 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 ∈ V)
31 opelxpi 4660 . . . . . . . . . 10 (((πΈβ€˜ndx) ∈ V ∧ 𝐢 ∈ V) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V))
3229, 30, 31sylancr 414 . . . . . . . . 9 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V))
33 relsng 4731 . . . . . . . . . 10 (⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V β†’ (Rel {⟨(πΈβ€˜ndx), 𝐢⟩} ↔ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V)))
3410, 33syl 14 . . . . . . . . 9 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (Rel {⟨(πΈβ€˜ndx), 𝐢⟩} ↔ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V)))
3532, 34mpbird 167 . . . . . . . 8 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ Rel {⟨(πΈβ€˜ndx), 𝐢⟩})
36 dmsnopg 5102 . . . . . . . . . 10 (𝐢 ∈ 𝑉 β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)})
3736adantl 277 . . . . . . . . 9 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)})
38 eqimss 3211 . . . . . . . . 9 (dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)} β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)})
3937, 38syl 14 . . . . . . . 8 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)})
40 relssres 4947 . . . . . . . 8 ((Rel {⟨(πΈβ€˜ndx), 𝐢⟩} ∧ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)}) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4135, 39, 40syl2anc 411 . . . . . . 7 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4228, 41uneq12d 3292 . . . . . 6 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) βˆͺ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)})) = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
43 resundir 4923 . . . . . 6 (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)}) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) βˆͺ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}))
44 un0 3458 . . . . . . 7 ({⟨(πΈβ€˜ndx), 𝐢⟩} βˆͺ βˆ…) = {⟨(πΈβ€˜ndx), 𝐢⟩}
45 uncom 3281 . . . . . . 7 ({⟨(πΈβ€˜ndx), 𝐢⟩} βˆͺ βˆ…) = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})
4644, 45eqtr3i 2200 . . . . . 6 {⟨(πΈβ€˜ndx), 𝐢⟩} = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})
4742, 43, 463eqtr4g 2235 . . . . 5 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4847fveq1d 5519 . . . 4 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ((((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)})β€˜(πΈβ€˜ndx)) = ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)))
4919, 48eqtr3id 2224 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)) = ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)))
50 fvsng 5714 . . . 4 (((πΈβ€˜ndx) ∈ β„• ∧ 𝐢 ∈ 𝑉) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)) = 𝐢)
512, 8, 50sylancr 414 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)) = 𝐢)
5249, 51eqtrd 2210 . 2 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)) = 𝐢)
535, 16, 523eqtrrd 2215 1 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 = (πΈβ€˜(π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩)))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  Vcvv 2739   βˆ– cdif 3128   βˆͺ cun 3129   ∩ cin 3130   βŠ† wss 3131  βˆ…c0 3424  {csn 3594  βŸ¨cop 3597   Γ— cxp 4626  dom cdm 4628   β†Ύ cres 4630  Rel wrel 4633  β€˜cfv 5218  (class class class)co 5877  β„•cn 8921  ndxcnx 12461   sSet csts 12462  Slot cslot 12463
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-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-iota 5180  df-fun 5220  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-slot 12468  df-sets 12471
This theorem is referenced by:  ressbasd  12529  mgpplusgg  13139  opprmulfvalg  13247  rmodislmod  13446  setsmstsetg  14066
  Copyright terms: Public domain W3C validator