Theorem setsid 17292

Description: Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)

Hypothesis

Ref	Expression
setsid.e	⊢ 𝐸 = Slot (𝐸‘ndx)

Assertion

Ref	Expression
setsid	⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))

Proof of Theorem setsid

Step	Hyp	Ref	Expression
1		setsval 17252	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
2	1	fveq2d 6892	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})))
3		setsid.e	. . 3 ⊢ 𝐸 = Slot (𝐸‘ndx)
4		resexg 6031	. . . . 5 ⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
5	4	adantr 486	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
6		snex 5415	. . . 4 ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V
7		unexg 7754	. . . 4 ⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
8	5, 6, 7	sylancl 598	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
9	3, 8	strfvnd 17270	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
10		fvex 6901	. . . . . 6 ⊢ (𝐸‘ndx) ∈ V
11	10	snid 4633	. . . . 5 ⊢ (𝐸‘ndx) ∈ {(𝐸‘ndx)}
12		fvres 6907	. . . . 5 ⊢ ((𝐸‘ndx) ∈ {(𝐸‘ndx)} → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
13	11, 12	ax-mp 5	. . . 4 ⊢ ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx))
14		resres 5996	. . . . . . . . 9 ⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}))
15		disjdifr 4437	. . . . . . . . . . 11 ⊢ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ∅
16	15	reseq2i 5980	. . . . . . . . . 10 ⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾ ∅)
17		res0 5987	. . . . . . . . . 10 ⊢ (𝑊 ↾ ∅) = ∅
18	16, 17	eqtri 2789	. . . . . . . . 9 ⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = ∅
19	14, 18	eqtri 2789	. . . . . . . 8 ⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅
20	19	a1i 11	. . . . . . 7 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅)
21		elex 3479	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V)
22	21	adantl 487	. . . . . . . . . 10 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V)
23		opelxpi 5703	. . . . . . . . . 10 ⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
24	10, 22, 23	sylancr 599	. . . . . . . . 9 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
25		opex 5450	. . . . . . . . . 10 ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ V
26	25	relsn 5796	. . . . . . . . 9 ⊢ (Rel {⟨(𝐸‘ndx), 𝐶⟩} ↔ ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
27	24, 26	sylibr 237	. . . . . . . 8 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {⟨(𝐸‘ndx), 𝐶⟩})
28		dmsnopss 6220	. . . . . . . 8 ⊢ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}
29		relssres 6026	. . . . . . . 8 ⊢ ((Rel {⟨(𝐸‘ndx), 𝐶⟩} ∧ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
30	27, 28, 29	sylancl 598	. . . . . . 7 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
31	20, 30	uneq12d 4126	. . . . . 6 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)})) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
32		resundir 5998	. . . . . 6 ⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}))
33		un0 4354	. . . . . . 7 ⊢ ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = {⟨(𝐸‘ndx), 𝐶⟩}
34		uncom 4115	. . . . . . 7 ⊢ ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
35	33, 34	eqtr3i 2791	. . . . . 6 ⊢ {⟨(𝐸‘ndx), 𝐶⟩} = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
36	31, 32, 35	3eqtr4g 2826	. . . . 5 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
37	36	fveq1d 6890	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
38	13, 37	eqtr3id 2815	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
39	10	a1i 11	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ V)
40		fvsng 7185	. . . 4 ⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
41	39, 40	sylancom 600	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
42	38, 41	eqtrd 2801	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = 𝐶)
43	2, 9, 42	3eqtrrd 2806	1 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3458   ∖ cdif 3905   ∪ cun 3906   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289  {csn 4594  ⟨cop 4600   × cxp 5664  dom cdm 5666   ↾ cres 5668  Rel wrel 5671  ‘cfv 6543  (class class class)co 7423   sSet csts 17248  Slot cslot 17266  ndxcnx 17278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-res 5678  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-sets 17249  df-slot 17267

This theorem is used by:  ressbas  17321  oppchomfval  17795  oppccofval  17797  reschom  17912  oduleval  18370  oppgplusfval  19449  mgpplusg  20251  opprmulfval  20454  rmodislmod  21088  srasca  21338  sravsca  21339  sraip  21340  zlmsca  21707  zlmvsca  21708  znle  21723  thloc  21886  opsrle  22235  matmulr  22632  tuslem  24460  setsmstset  24671  tngds  24842  tngtset  24843  ttgval  29261  setsiedg  29423  resvsca  33683  hlhilnvl  42764  mnringmulrd  44987  cznrng  49066  cznnring  49067  prstchomval  50377  prstcthin  50379