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

Theorem setsslid 12513
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 12493 . . . 4 ((π‘Š ∈ 𝐴 ∧ (πΈβ€˜ndx) ∈ β„• ∧ 𝐢 ∈ 𝑉) β†’ (π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩) = ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
42, 3mp3an2 1325 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩) = ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
54fveq2d 5520 . 2 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (πΈβ€˜(π‘Š sSet ⟨(πΈβ€˜ndx), 𝐢⟩)) = (πΈβ€˜((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})))
61simpli 111 . . 3 𝐸 = Slot (πΈβ€˜ndx)
7 resexg 4948 . . . 4 (π‘Š ∈ 𝐴 β†’ (π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) ∈ V)
8 simpr 110 . . . . . 6 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 ∈ 𝑉)
9 opexg 4229 . . . . . 6 (((πΈβ€˜ndx) ∈ β„• ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V)
102, 8, 9sylancr 414 . . . . 5 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V)
11 snexg 4185 . . . . 5 (⟨(πΈβ€˜ndx), 𝐢⟩ ∈ V β†’ {⟨(πΈβ€˜ndx), 𝐢⟩} ∈ V)
1210, 11syl 14 . . . 4 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ {⟨(πΈβ€˜ndx), 𝐢⟩} ∈ V)
13 unexg 4444 . . . 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 12482 . 2 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (πΈβ€˜((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)))
17 snidg 3622 . . . . 5 ((πΈβ€˜ndx) ∈ β„• β†’ (πΈβ€˜ndx) ∈ {(πΈβ€˜ndx)})
18 fvres 5540 . . . . 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 4920 . . . . . . . . 9 ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}))
21 incom 3328 . . . . . . . . . . . 12 ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}) = ({(πΈβ€˜ndx)} ∩ (V βˆ– {(πΈβ€˜ndx)}))
22 disjdif 3496 . . . . . . . . . . . 12 ({(πΈβ€˜ndx)} ∩ (V βˆ– {(πΈβ€˜ndx)})) = βˆ…
2321, 22eqtri 2198 . . . . . . . . . . 11 ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)}) = βˆ…
2423reseq2i 4905 . . . . . . . . . 10 (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)})) = (π‘Š β†Ύ βˆ…)
25 res0 4912 . . . . . . . . . 10 (π‘Š β†Ύ βˆ…) = βˆ…
2624, 25eqtri 2198 . . . . . . . . 9 (π‘Š β†Ύ ((V βˆ– {(πΈβ€˜ndx)}) ∩ {(πΈβ€˜ndx)})) = βˆ…
2720, 26eqtri 2198 . . . . . . . 8 ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = βˆ…
2827a1i 9 . . . . . . 7 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) = βˆ…)
292elexi 2750 . . . . . . . . . 10 (πΈβ€˜ndx) ∈ V
308elexd 2751 . . . . . . . . . 10 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ 𝐢 ∈ V)
31 opelxpi 4659 . . . . . . . . . 10 (((πΈβ€˜ndx) ∈ V ∧ 𝐢 ∈ V) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V))
3229, 30, 31sylancr 414 . . . . . . . . 9 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ⟨(πΈβ€˜ndx), 𝐢⟩ ∈ (V Γ— V))
33 relsng 4730 . . . . . . . . . 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 5101 . . . . . . . . . 10 (𝐢 ∈ 𝑉 β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)})
3736adantl 277 . . . . . . . . 9 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)})
38 eqimss 3210 . . . . . . . . 9 (dom {⟨(πΈβ€˜ndx), 𝐢⟩} = {(πΈβ€˜ndx)} β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)})
3937, 38syl 14 . . . . . . . 8 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)})
40 relssres 4946 . . . . . . . 8 ((Rel {⟨(πΈβ€˜ndx), 𝐢⟩} ∧ dom {⟨(πΈβ€˜ndx), 𝐢⟩} βŠ† {(πΈβ€˜ndx)}) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4135, 39, 40syl2anc 411 . . . . . . 7 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4228, 41uneq12d 3291 . . . . . 6 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) βˆͺ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)})) = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}))
43 resundir 4922 . . . . . 6 (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)}) = (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) β†Ύ {(πΈβ€˜ndx)}) βˆͺ ({⟨(πΈβ€˜ndx), 𝐢⟩} β†Ύ {(πΈβ€˜ndx)}))
44 un0 3457 . . . . . . 7 ({⟨(πΈβ€˜ndx), 𝐢⟩} βˆͺ βˆ…) = {⟨(πΈβ€˜ndx), 𝐢⟩}
45 uncom 3280 . . . . . . 7 ({⟨(πΈβ€˜ndx), 𝐢⟩} βˆͺ βˆ…) = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})
4644, 45eqtr3i 2200 . . . . . 6 {⟨(πΈβ€˜ndx), 𝐢⟩} = (βˆ… βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})
4742, 43, 463eqtr4g 2235 . . . . 5 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)}) = {⟨(πΈβ€˜ndx), 𝐢⟩})
4847fveq1d 5518 . . . 4 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ ((((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩}) β†Ύ {(πΈβ€˜ndx)})β€˜(πΈβ€˜ndx)) = ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)))
4919, 48eqtr3id 2224 . . 3 ((π‘Š ∈ 𝐴 ∧ 𝐢 ∈ 𝑉) β†’ (((π‘Š β†Ύ (V βˆ– {(πΈβ€˜ndx)})) βˆͺ {⟨(πΈβ€˜ndx), 𝐢⟩})β€˜(πΈβ€˜ndx)) = ({⟨(πΈβ€˜ndx), 𝐢⟩}β€˜(πΈβ€˜ndx)))
50 fvsng 5713 . . . 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 2738   βˆ– cdif 3127   βˆͺ cun 3128   ∩ cin 3129   βŠ† wss 3130  βˆ…c0 3423  {csn 3593  βŸ¨cop 3596   Γ— cxp 4625  dom cdm 4627   β†Ύ cres 4629  Rel wrel 4632  β€˜cfv 5217  (class class class)co 5875  β„•cn 8919  ndxcnx 12459   sSet csts 12460  Slot cslot 12461
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 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537
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 2740  df-sbc 2964  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-iota 5179  df-fun 5219  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-slot 12466  df-sets 12469
This theorem is referenced by:  ressbasd  12527  mgpplusgg  13134  opprmulfvalg  13242  rmodislmod  13441  setsmstsetg  13984
  Copyright terms: Public domain W3C validator