![]() |
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 17187 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx))) |
4 | ovex 7457 | . . . . 5 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) ∈ V | |
5 | 4, 1 | strfvn 17188 | . . . 4 ⊢ (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
6 | setsres 17180 | . . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷}))) | |
7 | 6 | fveq1d 6903 | . . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx))) |
8 | fvex 6914 | . . . . . . 7 ⊢ (𝐸‘ndx) ∈ V | |
9 | setsnid.n | . . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷 | |
10 | eldifsn 4795 | . . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷)) | |
11 | 8, 9, 10 | mpbir2an 709 | . . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷}) |
12 | fvres 6920 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx))) | |
13 | 11, 12 | ax-mp 5 | . . . . 5 ⊢ (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
14 | fvres 6920 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) | |
15 | 11, 14 | ax-mp 5 | . . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)) |
16 | 7, 13, 15 | 3eqtr3g 2789 | . . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) |
17 | 5, 16 | eqtrid 2778 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝑊‘(𝐸‘ndx))) |
18 | 3, 17 | eqtr4d 2769 | . 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
19 | 1 | str0 17191 | . . . 4 ⊢ ∅ = (𝐸‘∅) |
20 | 19 | eqcomi 2735 | . . 3 ⊢ (𝐸‘∅) = ∅ |
21 | eqid 2726 | . . 3 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) = (𝑊 sSet 〈𝐷, 𝐶〉) | |
22 | reldmsets 17167 | . . 3 ⊢ Rel dom sSet | |
23 | 20, 21, 22 | oveqprc 17194 | . 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
24 | 18, 23 | pm2.61i 182 | 1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 ≠ wne 2930 Vcvv 3462 ∖ cdif 3944 ∅c0 4325 {csn 4633 〈cop 4639 ↾ cres 5684 ‘cfv 6554 (class class class)co 7424 sSet csts 17165 Slot cslot 17183 ndxcnx 17195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-res 5694 df-iota 6506 df-fun 6556 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-sets 17166 df-slot 17184 |
This theorem is referenced by: resseqnbas 17255 resslemOLD 17256 oppchomfval 17727 oppchomfvalOLD 17728 oppcbas 17732 oppcbasOLD 17733 rescbas 17845 rescbasOLD 17846 rescco 17849 resccoOLD 17850 rescabs 17851 rescabsOLD 17852 odubas 18316 odubasOLD 18317 setsplusg 19344 oppglemOLD 19345 mgplemOLD 20122 opprlem 20321 opprlemOLD 20322 rmodislmod 20906 rmodislmodOLD 20907 sralem 21154 sralemOLD 21155 srasca 21162 srascaOLD 21163 sravsca 21164 sravscaOLD 21165 zlmlem 21506 zlmlemOLD 21507 zlmsca 21514 znbaslem 21532 znbaslemOLD 21533 thlbas 21692 thlbasOLD 21693 thlle 21694 thlleOLD 21695 opsrbaslem 22056 opsrbaslemOLD 22057 matbas 22404 matplusg 22405 matsca 22406 matscaOLD 22407 matvsca 22408 matvscaOLD 22409 tuslem 24262 tuslemOLD 24263 setsmsbas 24472 setsmsbasOLD 24473 setsmsds 24474 setsmsdsOLD 24475 tnglem 24640 tnglemOLD 24641 tngds 24655 tngdsOLD 24656 ttgval 28802 ttgvalOLD 28803 ttglem 28804 ttglemOLD 28805 cchhllem 28820 cchhllemOLD 28821 setsvtx 28971 resvlem 33205 resvlemOLD 33206 zlmds 33777 zlmdsOLD 33778 zlmtset 33779 zlmtsetOLD 33780 hlhilslem 41637 hlhilslemOLD 41638 mnringnmulrd 43883 mnringnmulrdOLD 43884 cznrnglem 47636 cznabel 47637 cznrng 47638 prstcnidlem 48386 prstcnid 48387 |
Copyright terms: Public domain | W3C validator |