![]() |
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 17122 | . . 3 β’ (π β V β (πΈβπ) = (πβ(πΈβndx))) |
4 | ovex 7444 | . . . . 5 β’ (π sSet β¨π·, πΆβ©) β V | |
5 | 4, 1 | strfvn 17123 | . . . 4 β’ (πΈβ(π sSet β¨π·, πΆβ©)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx)) |
6 | setsres 17115 | . . . . . 6 β’ (π β V β ((π sSet β¨π·, πΆβ©) βΎ (V β {π·})) = (π βΎ (V β {π·}))) | |
7 | 6 | fveq1d 6892 | . . . . 5 β’ (π β V β (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π βΎ (V β {π·}))β(πΈβndx))) |
8 | fvex 6903 | . . . . . . 7 β’ (πΈβndx) β V | |
9 | setsnid.n | . . . . . . 7 β’ (πΈβndx) β π· | |
10 | eldifsn 4789 | . . . . . . 7 β’ ((πΈβndx) β (V β {π·}) β ((πΈβndx) β V β§ (πΈβndx) β π·)) | |
11 | 8, 9, 10 | mpbir2an 707 | . . . . . 6 β’ (πΈβndx) β (V β {π·}) |
12 | fvres 6909 | . . . . . 6 β’ ((πΈβndx) β (V β {π·}) β (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx))) | |
13 | 11, 12 | ax-mp 5 | . . . . 5 β’ (((π sSet β¨π·, πΆβ©) βΎ (V β {π·}))β(πΈβndx)) = ((π sSet β¨π·, πΆβ©)β(πΈβndx)) |
14 | fvres 6909 | . . . . . 6 β’ ((πΈβndx) β (V β {π·}) β ((π βΎ (V β {π·}))β(πΈβndx)) = (πβ(πΈβndx))) | |
15 | 11, 14 | ax-mp 5 | . . . . 5 β’ ((π βΎ (V β {π·}))β(πΈβndx)) = (πβ(πΈβndx)) |
16 | 7, 13, 15 | 3eqtr3g 2793 | . . . 4 β’ (π β V β ((π sSet β¨π·, πΆβ©)β(πΈβndx)) = (πβ(πΈβndx))) |
17 | 5, 16 | eqtrid 2782 | . . 3 β’ (π β V β (πΈβ(π sSet β¨π·, πΆβ©)) = (πβ(πΈβndx))) |
18 | 3, 17 | eqtr4d 2773 | . 2 β’ (π β V β (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©))) |
19 | 1 | str0 17126 | . . . 4 β’ β = (πΈββ ) |
20 | 19 | eqcomi 2739 | . . 3 β’ (πΈββ ) = β |
21 | eqid 2730 | . . 3 β’ (π sSet β¨π·, πΆβ©) = (π sSet β¨π·, πΆβ©) | |
22 | reldmsets 17102 | . . 3 β’ Rel dom sSet | |
23 | 20, 21, 22 | oveqprc 17129 | . 2 β’ (Β¬ π β V β (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©))) |
24 | 18, 23 | pm2.61i 182 | 1 β’ (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 β wcel 2104 β wne 2938 Vcvv 3472 β cdif 3944 β c0 4321 {csn 4627 β¨cop 4633 βΎ cres 5677 βcfv 6542 (class class class)co 7411 sSet csts 17100 Slot cslot 17118 ndxcnx 17130 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-res 5687 df-iota 6494 df-fun 6544 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-sets 17101 df-slot 17119 |
This theorem is referenced by: resseqnbas 17190 resslemOLD 17191 oppchomfval 17662 oppchomfvalOLD 17663 oppcbas 17667 oppcbasOLD 17668 rescbas 17780 rescbasOLD 17781 rescco 17784 resccoOLD 17785 rescabs 17786 rescabsOLD 17787 odubas 18248 odubasOLD 18249 setsplusg 19255 oppglemOLD 19256 mgplemOLD 20033 opprlem 20230 opprlemOLD 20231 rmodislmod 20684 rmodislmodOLD 20685 sralem 20935 sralemOLD 20936 srasca 20943 srascaOLD 20944 sravsca 20945 sravscaOLD 20946 zlmlem 21285 zlmlemOLD 21286 zlmsca 21293 znbaslem 21309 znbaslemOLD 21310 thlbas 21468 thlbasOLD 21469 thlle 21470 thlleOLD 21471 opsrbaslem 21823 opsrbaslemOLD 21824 matbas 22133 matplusg 22134 matsca 22135 matscaOLD 22136 matvsca 22137 matvscaOLD 22138 tuslem 23991 tuslemOLD 23992 setsmsbas 24201 setsmsbasOLD 24202 setsmsds 24203 setsmsdsOLD 24204 tnglem 24369 tnglemOLD 24370 tngds 24384 tngdsOLD 24385 ttgval 28393 ttgvalOLD 28394 ttglem 28395 ttglemOLD 28396 cchhllem 28411 cchhllemOLD 28412 setsvtx 28562 resvlem 32715 resvlemOLD 32716 zlmds 33240 zlmdsOLD 33241 zlmtset 33242 zlmtsetOLD 33243 hlhilslem 41112 hlhilslemOLD 41113 mnringnmulrd 43270 mnringnmulrdOLD 43271 cznrnglem 46939 cznabel 46940 cznrng 46941 prstcnidlem 47772 prstcnid 47773 |
Copyright terms: Public domain | W3C validator |