| 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 17112 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx))) |
| 4 | ovex 7391 | . . . . 5 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) ∈ V | |
| 5 | 4, 1 | strfvn 17113 | . . . 4 ⊢ (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
| 6 | setsres 17105 | . . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷}))) | |
| 7 | 6 | fveq1d 6836 | . . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx))) |
| 8 | fvex 6847 | . . . . . . 7 ⊢ (𝐸‘ndx) ∈ V | |
| 9 | setsnid.n | . . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷 | |
| 10 | eldifsn 4742 | . . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷)) | |
| 11 | 8, 9, 10 | mpbir2an 711 | . . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷}) |
| 12 | fvres 6853 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx))) | |
| 13 | 11, 12 | ax-mp 5 | . . . . 5 ⊢ (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
| 14 | fvres 6853 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) | |
| 15 | 11, 14 | ax-mp 5 | . . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)) |
| 16 | 7, 13, 15 | 3eqtr3g 2794 | . . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) |
| 17 | 5, 16 | eqtrid 2783 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝑊‘(𝐸‘ndx))) |
| 18 | 3, 17 | eqtr4d 2774 | . 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
| 19 | 1 | str0 17116 | . . . 4 ⊢ ∅ = (𝐸‘∅) |
| 20 | 19 | eqcomi 2745 | . . 3 ⊢ (𝐸‘∅) = ∅ |
| 21 | eqid 2736 | . . 3 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) = (𝑊 sSet 〈𝐷, 𝐶〉) | |
| 22 | reldmsets 17092 | . . 3 ⊢ Rel dom sSet | |
| 23 | 20, 21, 22 | oveqprc 17119 | . 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
| 24 | 18, 23 | pm2.61i 182 | 1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1541 ∈ wcel 2113 ≠ wne 2932 Vcvv 3440 ∖ cdif 3898 ∅c0 4285 {csn 4580 〈cop 4586 ↾ cres 5626 ‘cfv 6492 (class class class)co 7358 sSet csts 17090 Slot cslot 17108 ndxcnx 17120 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-sbc 3741 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-res 5636 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7361 df-oprab 7362 df-mpo 7363 df-sets 17091 df-slot 17109 |
| This theorem is referenced by: resseqnbas 17169 oppchomfval 17637 oppcbas 17641 rescbas 17753 rescco 17756 rescabs 17757 odubas 18214 setsplusg 19279 opprlem 20278 rmodislmod 20881 sralem 21128 srasca 21132 sravsca 21133 zlmlem 21471 zlmsca 21475 znbaslem 21493 thlbas 21651 thlle 21652 opsrbaslem 22004 matbas 22357 matplusg 22358 matsca 22359 matvsca 22360 tuslem 24210 setsmsbas 24419 setsmsds 24420 tnglem 24584 tngds 24592 ttgval 28947 ttglem 28948 cchhllem 28959 setsvtx 29108 resvlem 33414 zlmds 34119 zlmtset 34120 hlhilslem 42208 mnringnmulrd 44465 cznrnglem 48515 cznabel 48516 cznrng 48517 prstcnidlem 49807 prstcnid 49808 |
| Copyright terms: Public domain | W3C validator |