Theorem setsid 16372

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 16347	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩) = ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
2	1	fveq2d 6547	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)) = (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})))
3		setsid.e	. . 3 ⊢ 𝐸 = Slot (𝐸‘ndx)
4		resexg 5784	. . . . 5 ⊢ (𝑊 ∈ 𝐴 → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
5	4	adantr 481	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V)
6		snex 5228	. . . 4 ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V
7		unexg 7334	. . . 4 ⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∈ V ∧ {⟨(𝐸‘ndx), 𝐶⟩} ∈ V) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
8	5, 6, 7	sylancl 586	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ∈ V)
9	3, 8	strfvnd 16336	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)))
10		fvex 6556	. . . . . 6 ⊢ (𝐸‘ndx) ∈ V
11	10	snid 4510	. . . . 5 ⊢ (𝐸‘ndx) ∈ {(𝐸‘ndx)}
12		fvres 6562	. . . . 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 5752	. . . . . . . . 9 ⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}))
15		incom 4103	. . . . . . . . . . . 12 ⊢ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)}))
16		disjdif 4339	. . . . . . . . . . . 12 ⊢ ({(𝐸‘ndx)} ∩ (V ∖ {(𝐸‘ndx)})) = ∅
17	15, 16	eqtri 2819	. . . . . . . . . . 11 ⊢ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)}) = ∅
18	17	reseq2i 5736	. . . . . . . . . 10 ⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = (𝑊 ↾ ∅)
19		res0 5743	. . . . . . . . . 10 ⊢ (𝑊 ↾ ∅) = ∅
20	18, 19	eqtri 2819	. . . . . . . . 9 ⊢ (𝑊 ↾ ((V ∖ {(𝐸‘ndx)}) ∩ {(𝐸‘ndx)})) = ∅
21	14, 20	eqtri 2819	. . . . . . . 8 ⊢ ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅
22	21	a1i 11	. . . . . . 7 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) = ∅)
23		elex 3455	. . . . . . . . . . 11 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V)
24	23	adantl 482	. . . . . . . . . 10 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ V)
25		opelxpi 5485	. . . . . . . . . 10 ⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ V) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
26	10, 24, 25	sylancr 587	. . . . . . . . 9 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
27		opex 5253	. . . . . . . . . 10 ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ V
28	27	relsn 5568	. . . . . . . . 9 ⊢ (Rel {⟨(𝐸‘ndx), 𝐶⟩} ↔ ⟨(𝐸‘ndx), 𝐶⟩ ∈ (V × V))
29	26, 28	sylibr 235	. . . . . . . 8 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → Rel {⟨(𝐸‘ndx), 𝐶⟩})
30		dmsnopss 5951	. . . . . . . 8 ⊢ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}
31		relssres 5779	. . . . . . . 8 ⊢ ((Rel {⟨(𝐸‘ndx), 𝐶⟩} ∧ dom {⟨(𝐸‘ndx), 𝐶⟩} ⊆ {(𝐸‘ndx)}) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
32	29, 30, 31	sylancl 586	. . . . . . 7 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
33	22, 32	uneq12d 4065	. . . . . 6 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)})) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩}))
34		resundir 5754	. . . . . 6 ⊢ (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ↾ {(𝐸‘ndx)}) ∪ ({⟨(𝐸‘ndx), 𝐶⟩} ↾ {(𝐸‘ndx)}))
35		un0 4268	. . . . . . 7 ⊢ ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = {⟨(𝐸‘ndx), 𝐶⟩}
36		uncom 4054	. . . . . . 7 ⊢ ({⟨(𝐸‘ndx), 𝐶⟩} ∪ ∅) = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
37	35, 36	eqtr3i 2821	. . . . . 6 ⊢ {⟨(𝐸‘ndx), 𝐶⟩} = (∅ ∪ {⟨(𝐸‘ndx), 𝐶⟩})
38	33, 34, 37	3eqtr4g 2856	. . . . 5 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)}) = {⟨(𝐸‘ndx), 𝐶⟩})
39	38	fveq1d 6545	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ((((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩}) ↾ {(𝐸‘ndx)})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
40	13, 39	syl5eqr 2845	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)))
41	10	a1i 11	. . . 4 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘ndx) ∈ V)
42		fvsng 6810	. . . 4 ⊢ (((𝐸‘ndx) ∈ V ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
43	41, 42	sylancom 588	. . 3 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → ({⟨(𝐸‘ndx), 𝐶⟩}‘(𝐸‘ndx)) = 𝐶)
44	40, 43	eqtrd 2831	. 2 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (((𝑊 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), 𝐶⟩})‘(𝐸‘ndx)) = 𝐶)
45	2, 9, 44	3eqtrrd 2836	1 ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2081  Vcvv 3437   ∖ cdif 3860   ∪ cun 3861   ∩ cin 3862   ⊆ wss 3863  ∅c0 4215  {csn 4476  ⟨cop 4482   × cxp 5446  dom cdm 5448   ↾ cres 5450  Rel wrel 5453  ‘cfv 6230  (class class class)co 7021  ndxcnx 16314   sSet csts 16315  Slot cslot 16316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-res 5460  df-iota 6194  df-fun 6232  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-slot 16321  df-sets 16324

This theorem is referenced by:  ressbas  16388  oppchomfval  16818  oppccofval  16820  reschom  16934  oduleval  17575  oppgplusfval  18222  mgpplusg  18938  opprmulfval  19070  rmodislmod  19397  srasca  19648  sravsca  19649  sraip  19650  opsrle  19948  zlmsca  20355  zlmvsca  20356  znle  20370  thloc  20530  matmulr  20736  tuslem  22564  setsmstset  22775  tngds  22945  tngtset  22946  ttgval  26349  setsiedg  26509  resvsca  30562  hlhilnvl  38642  cznrng  43730  cznnring  43731