| 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 17161 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx))) |
| 4 | ovex 7422 | . . . . 5 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) ∈ V | |
| 5 | 4, 1 | strfvn 17162 | . . . 4 ⊢ (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
| 6 | setsres 17154 | . . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷}))) | |
| 7 | 6 | fveq1d 6862 | . . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx))) |
| 8 | fvex 6873 | . . . . . . 7 ⊢ (𝐸‘ndx) ∈ V | |
| 9 | setsnid.n | . . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷 | |
| 10 | eldifsn 4752 | . . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷)) | |
| 11 | 8, 9, 10 | mpbir2an 711 | . . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷}) |
| 12 | fvres 6879 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx))) | |
| 13 | 11, 12 | ax-mp 5 | . . . . 5 ⊢ (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
| 14 | fvres 6879 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) | |
| 15 | 11, 14 | ax-mp 5 | . . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)) |
| 16 | 7, 13, 15 | 3eqtr3g 2788 | . . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) |
| 17 | 5, 16 | eqtrid 2777 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝑊‘(𝐸‘ndx))) |
| 18 | 3, 17 | eqtr4d 2768 | . 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
| 19 | 1 | str0 17165 | . . . 4 ⊢ ∅ = (𝐸‘∅) |
| 20 | 19 | eqcomi 2739 | . . 3 ⊢ (𝐸‘∅) = ∅ |
| 21 | eqid 2730 | . . 3 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) = (𝑊 sSet 〈𝐷, 𝐶〉) | |
| 22 | reldmsets 17141 | . . 3 ⊢ Rel dom sSet | |
| 23 | 20, 21, 22 | oveqprc 17168 | . 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
| 24 | 18, 23 | pm2.61i 182 | 1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2109 ≠ wne 2926 Vcvv 3450 ∖ cdif 3913 ∅c0 4298 {csn 4591 〈cop 4597 ↾ cres 5642 ‘cfv 6513 (class class class)co 7389 sSet csts 17139 Slot cslot 17157 ndxcnx 17169 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5253 ax-nul 5263 ax-pr 5389 ax-un 7713 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3756 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-nul 4299 df-if 4491 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-br 5110 df-opab 5172 df-mpt 5191 df-id 5535 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-res 5652 df-iota 6466 df-fun 6515 df-fv 6521 df-ov 7392 df-oprab 7393 df-mpo 7394 df-sets 17140 df-slot 17158 |
| This theorem is referenced by: resseqnbas 17218 oppchomfval 17681 oppcbas 17685 rescbas 17797 rescco 17800 rescabs 17801 odubas 18258 setsplusg 19288 opprlem 20257 rmodislmod 20842 sralem 21089 srasca 21093 sravsca 21094 zlmlem 21432 zlmsca 21436 znbaslem 21454 thlbas 21611 thlle 21612 opsrbaslem 21962 matbas 22306 matplusg 22307 matsca 22308 matvsca 22309 tuslem 24160 setsmsbas 24369 setsmsds 24370 tnglem 24534 tngds 24542 ttgval 28808 ttglem 28809 cchhllem 28820 setsvtx 28968 resvlem 33311 zlmds 33958 zlmtset 33959 hlhilslem 41927 mnringnmulrd 44196 cznrnglem 48237 cznabel 48238 cznrng 48239 prstcnidlem 49521 prstcnid 49522 |
| Copyright terms: Public domain | W3C validator |