![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > setsnid | Structured version Visualization version GIF version |
Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 7-Nov-2024.) |
Ref | Expression |
---|---|
setsid.e | ⊢ 𝐸 = Slot (𝐸‘ndx) |
setsnid.n | ⊢ (𝐸‘ndx) ≠ 𝐷 |
Ref | Expression |
---|---|
setsnid | ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setsid.e | . . . 4 ⊢ 𝐸 = Slot (𝐸‘ndx) | |
2 | id 22 | . . . 4 ⊢ (𝑊 ∈ V → 𝑊 ∈ V) | |
3 | 1, 2 | strfvnd 17219 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx))) |
4 | ovex 7464 | . . . . 5 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) ∈ V | |
5 | 4, 1 | strfvn 17220 | . . . 4 ⊢ (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
6 | setsres 17212 | . . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷}))) | |
7 | 6 | fveq1d 6909 | . . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx))) |
8 | fvex 6920 | . . . . . . 7 ⊢ (𝐸‘ndx) ∈ V | |
9 | setsnid.n | . . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷 | |
10 | eldifsn 4791 | . . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷)) | |
11 | 8, 9, 10 | mpbir2an 711 | . . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷}) |
12 | fvres 6926 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx))) | |
13 | 11, 12 | ax-mp 5 | . . . . 5 ⊢ (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
14 | fvres 6926 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) | |
15 | 11, 14 | ax-mp 5 | . . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)) |
16 | 7, 13, 15 | 3eqtr3g 2798 | . . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) |
17 | 5, 16 | eqtrid 2787 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝑊‘(𝐸‘ndx))) |
18 | 3, 17 | eqtr4d 2778 | . 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
19 | 1 | str0 17223 | . . . 4 ⊢ ∅ = (𝐸‘∅) |
20 | 19 | eqcomi 2744 | . . 3 ⊢ (𝐸‘∅) = ∅ |
21 | eqid 2735 | . . 3 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) = (𝑊 sSet 〈𝐷, 𝐶〉) | |
22 | reldmsets 17199 | . . 3 ⊢ Rel dom sSet | |
23 | 20, 21, 22 | oveqprc 17226 | . 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
24 | 18, 23 | pm2.61i 182 | 1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∈ wcel 2106 ≠ wne 2938 Vcvv 3478 ∖ cdif 3960 ∅c0 4339 {csn 4631 〈cop 4637 ↾ cres 5691 ‘cfv 6563 (class class class)co 7431 sSet csts 17197 Slot cslot 17215 ndxcnx 17227 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-sbc 3792 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5583 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-res 5701 df-iota 6516 df-fun 6565 df-fv 6571 df-ov 7434 df-oprab 7435 df-mpo 7436 df-sets 17198 df-slot 17216 |
This theorem is referenced by: resseqnbas 17287 resslemOLD 17288 oppchomfval 17759 oppchomfvalOLD 17760 oppcbas 17764 oppcbasOLD 17765 rescbas 17877 rescbasOLD 17878 rescco 17881 resccoOLD 17882 rescabs 17883 rescabsOLD 17884 odubas 18348 odubasOLD 18349 setsplusg 19381 oppglemOLD 19382 mgplemOLD 20157 opprlem 20356 opprlemOLD 20357 rmodislmod 20945 rmodislmodOLD 20946 sralem 21193 sralemOLD 21194 srasca 21201 srascaOLD 21202 sravsca 21203 sravscaOLD 21204 zlmlem 21545 zlmlemOLD 21546 zlmsca 21553 znbaslem 21571 znbaslemOLD 21572 thlbas 21732 thlbasOLD 21733 thlle 21734 thlleOLD 21735 opsrbaslem 22085 opsrbaslemOLD 22086 matbas 22433 matplusg 22434 matsca 22435 matscaOLD 22436 matvsca 22437 matvscaOLD 22438 tuslem 24291 tuslemOLD 24292 setsmsbas 24501 setsmsbasOLD 24502 setsmsds 24503 setsmsdsOLD 24504 tnglem 24669 tnglemOLD 24670 tngds 24684 tngdsOLD 24685 ttgval 28898 ttgvalOLD 28899 ttglem 28900 ttglemOLD 28901 cchhllem 28916 cchhllemOLD 28917 setsvtx 29067 resvlem 33337 resvlemOLD 33338 zlmds 33923 zlmdsOLD 33924 zlmtset 33925 zlmtsetOLD 33926 hlhilslem 41921 hlhilslemOLD 41922 mnringnmulrd 44205 mnringnmulrdOLD 44206 cznrnglem 48103 cznabel 48104 cznrng 48105 prstcnidlem 48866 prstcnid 48867 |
Copyright terms: Public domain | W3C validator |