![]() |
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.) |
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 16348 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝑊‘(𝐸‘ndx))) |
4 | ovex 7002 | . . . . 5 ⊢ (𝑊 sSet 〈𝐷, 𝐶〉) ∈ V | |
5 | 4, 1 | strfvn 16351 | . . . 4 ⊢ (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
6 | setsres 16371 | . . . . . 6 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷})) = (𝑊 ↾ (V ∖ {𝐷}))) | |
7 | 6 | fveq1d 6495 | . . . . 5 ⊢ (𝑊 ∈ V → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx))) |
8 | fvex 6506 | . . . . . . 7 ⊢ (𝐸‘ndx) ∈ V | |
9 | setsnid.n | . . . . . . 7 ⊢ (𝐸‘ndx) ≠ 𝐷 | |
10 | eldifsn 4587 | . . . . . . 7 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) ↔ ((𝐸‘ndx) ∈ V ∧ (𝐸‘ndx) ≠ 𝐷)) | |
11 | 8, 9, 10 | mpbir2an 698 | . . . . . 6 ⊢ (𝐸‘ndx) ∈ (V ∖ {𝐷}) |
12 | fvres 6512 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx))) | |
13 | 11, 12 | ax-mp 5 | . . . . 5 ⊢ (((𝑊 sSet 〈𝐷, 𝐶〉) ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) |
14 | fvres 6512 | . . . . . 6 ⊢ ((𝐸‘ndx) ∈ (V ∖ {𝐷}) → ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) | |
15 | 11, 14 | ax-mp 5 | . . . . 5 ⊢ ((𝑊 ↾ (V ∖ {𝐷}))‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx)) |
16 | 7, 13, 15 | 3eqtr3g 2831 | . . . 4 ⊢ (𝑊 ∈ V → ((𝑊 sSet 〈𝐷, 𝐶〉)‘(𝐸‘ndx)) = (𝑊‘(𝐸‘ndx))) |
17 | 5, 16 | syl5eq 2820 | . . 3 ⊢ (𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝑊‘(𝐸‘ndx))) |
18 | 3, 17 | eqtr4d 2811 | . 2 ⊢ (𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
19 | 1 | str0 16381 | . . 3 ⊢ ∅ = (𝐸‘∅) |
20 | fvprc 6486 | . . 3 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = ∅) | |
21 | reldmsets 16357 | . . . . 5 ⊢ Rel dom sSet | |
22 | 21 | ovprc1 7008 | . . . 4 ⊢ (¬ 𝑊 ∈ V → (𝑊 sSet 〈𝐷, 𝐶〉) = ∅) |
23 | 22 | fveq2d 6497 | . . 3 ⊢ (¬ 𝑊 ∈ V → (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) = (𝐸‘∅)) |
24 | 19, 20, 23 | 3eqtr4a 2834 | . 2 ⊢ (¬ 𝑊 ∈ V → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) |
25 | 18, 24 | pm2.61i 177 | 1 ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1507 ∈ wcel 2048 ≠ wne 2961 Vcvv 3409 ∖ cdif 3822 ∅c0 4173 {csn 4435 〈cop 4441 ↾ cres 5402 ‘cfv 6182 (class class class)co 6970 ndxcnx 16326 sSet csts 16327 Slot cslot 16328 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3678 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-res 5412 df-iota 6146 df-fun 6184 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-slot 16333 df-sets 16336 |
This theorem is referenced by: resslem 16403 oppchomfval 16832 oppcbas 16836 rescbas 16947 rescco 16950 rescabs 16951 odubas 17591 oppglem 18239 mgplem 18957 opprlem 19091 rmodislmod 19414 sralem 19661 srasca 19665 sravsca 19666 opsrbaslem 19961 zlmlem 20356 zlmsca 20360 znbaslem 20377 thlbas 20532 thlle 20533 matbas 20716 matplusg 20717 matsca 20718 matvsca 20719 tuslem 22569 setsmsbas 22778 setsmsds 22779 tnglem 22942 tngds 22950 ttgval 26354 ttglem 26355 cchhllem 26366 setsvtx 26513 resvlem 30539 zlmds 30806 zlmtset 30807 hlhilslem 38467 cznrnglem 43528 cznabel 43529 cznrng 43530 |
Copyright terms: Public domain | W3C validator |