Theorem strsetsid 13138

Description: Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)

Hypotheses

Ref	Expression
strsetsid.e	⊢ 𝐸 = Slot (𝐸‘ndx)
strsetsid.s	⊢ (𝜑 → 𝑆 Struct ⟨𝑀, 𝑁⟩)
strsetsid.f	⊢ (𝜑 → Fun 𝑆)
strsetsid.d	⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆)

Assertion

Ref	Expression
strsetsid	⊢ (𝜑 → 𝑆 = (𝑆 sSet ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩))

Proof of Theorem strsetsid

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		strsetsid.s	. . . 4 ⊢ (𝜑 → 𝑆 Struct ⟨𝑀, 𝑁⟩)
2		structex 13117	. . . 4 ⊢ (𝑆 Struct ⟨𝑀, 𝑁⟩ → 𝑆 ∈ V)
3	1, 2	syl 14	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
4		strsetsid.d	. . 3 ⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆)
5		strsetsid.e	. . . . 5 ⊢ 𝐸 = Slot (𝐸‘ndx)
6		isstructim 13119	. . . . . . . . 9 ⊢ (𝑆 Struct ⟨𝑀, 𝑁⟩ → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝑆 ∖ {∅}) ∧ dom 𝑆 ⊆ (𝑀...𝑁)))
7	1, 6	syl 14	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝑆 ∖ {∅}) ∧ dom 𝑆 ⊆ (𝑀...𝑁)))
8	7	simp3d 1037	. . . . . . 7 ⊢ (𝜑 → dom 𝑆 ⊆ (𝑀...𝑁))
9	7	simp1d 1035	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁))
10	9	simp1d 1035	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11		fzssnn 10308	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑀...𝑁) ⊆ ℕ)
12	10, 11	syl 14	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑁) ⊆ ℕ)
13	8, 12	sstrd 3236	. . . . . 6 ⊢ (𝜑 → dom 𝑆 ⊆ ℕ)
14	13, 4	sseldd 3227	. . . . 5 ⊢ (𝜑 → (𝐸‘ndx) ∈ ℕ)
15	5, 3, 14	strnfvnd 13125	. . . 4 ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘(𝐸‘ndx)))
16		strsetsid.f	. . . . 5 ⊢ (𝜑 → Fun 𝑆)
17		funfvex 5659	. . . . 5 ⊢ ((Fun 𝑆 ∧ (𝐸‘ndx) ∈ dom 𝑆) → (𝑆‘(𝐸‘ndx)) ∈ V)
18	16, 4, 17	syl2anc 411	. . . 4 ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) ∈ V)
19	15, 18	eqeltrd 2307	. . 3 ⊢ (𝜑 → (𝐸‘𝑆) ∈ V)
20		setsvala 13136	. . 3 ⊢ ((𝑆 ∈ V ∧ (𝐸‘ndx) ∈ dom 𝑆 ∧ (𝐸‘𝑆) ∈ V) → (𝑆 sSet ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝐸‘𝑆)⟩}))
21	3, 4, 19, 20	syl3anc 1273	. 2 ⊢ (𝜑 → (𝑆 sSet ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝐸‘𝑆)⟩}))
22	15	opeq2d 3870	. . . 4 ⊢ (𝜑 → ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩ = ⟨(𝐸‘ndx), (𝑆‘(𝐸‘ndx))⟩)
23	22	sneqd 3683	. . 3 ⊢ (𝜑 → {⟨(𝐸‘ndx), (𝐸‘𝑆)⟩} = {⟨(𝐸‘ndx), (𝑆‘(𝐸‘ndx))⟩})
24	23	uneq2d 3360	. 2 ⊢ (𝜑 → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝐸‘𝑆)⟩}) = ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝑆‘(𝐸‘ndx))⟩}))
25		nnssz 9501	. . . . 5 ⊢ ℕ ⊆ ℤ
26	13, 25	sstrdi 3238	. . . 4 ⊢ (𝜑 → dom 𝑆 ⊆ ℤ)
27		zdceq 9560	. . . . 5 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → DECID 𝑥 = 𝑦)
28	27	rgen2a 2585	. . . 4 ⊢ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ DECID 𝑥 = 𝑦
29		ssralv 3290	. . . . . 6 ⊢ (dom 𝑆 ⊆ ℤ → (∀𝑦 ∈ ℤ DECID 𝑥 = 𝑦 → ∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦))
30	29	ralimdv 2599	. . . . 5 ⊢ (dom 𝑆 ⊆ ℤ → (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ DECID 𝑥 = 𝑦 → ∀𝑥 ∈ ℤ ∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦))
31		ssralv 3290	. . . . 5 ⊢ (dom 𝑆 ⊆ ℤ → (∀𝑥 ∈ ℤ ∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦))
32	30, 31	syld 45	. . . 4 ⊢ (dom 𝑆 ⊆ ℤ → (∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ DECID 𝑥 = 𝑦 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦))
33	26, 28, 32	mpisyl 1491	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦)
34		funresdfunsndc 6679	. . 3 ⊢ ((∀𝑥 ∈ dom 𝑆∀𝑦 ∈ dom 𝑆DECID 𝑥 = 𝑦 ∧ Fun 𝑆 ∧ (𝐸‘ndx) ∈ dom 𝑆) → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝑆‘(𝐸‘ndx))⟩}) = 𝑆)
35	33, 16, 4, 34	syl3anc 1273	. 2 ⊢ (𝜑 → ((𝑆 ↾ (V ∖ {(𝐸‘ndx)})) ∪ {⟨(𝐸‘ndx), (𝑆‘(𝐸‘ndx))⟩}) = 𝑆)
36	21, 24, 35	3eqtrrd 2268	1 ⊢ (𝜑 → 𝑆 = (𝑆 sSet ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩))

Syntax hints:   → wi 4  DECID wdc 841   ∧ w3a 1004   = wceq 1397   ∈ wcel 2201  ∀wral 2509  Vcvv 2801   ∖ cdif 3196   ∪ cun 3197   ⊆ wss 3199  ∅c0 3493  {csn 3670  ⟨cop 3673   class class class wbr 4089  dom cdm 4727   ↾ cres 4729  Fun wfun 5322  ‘cfv 5328  (class class class)co 6023   ≤ cle 8220  ℕcn 9148  ℤcz 9484  ...cfz 10248   Struct cstr 13101  ndxcnx 13102   sSet csts 13103  Slot cslot 13104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-cnex 8128  ax-resscn 8129  ax-1cn 8130  ax-1re 8131  ax-icn 8132  ax-addcl 8133  ax-addrcl 8134  ax-mulcl 8135  ax-addcom 8137  ax-addass 8139  ax-distr 8141  ax-i2m1 8142  ax-0lt1 8143  ax-0id 8145  ax-rnegex 8146  ax-cnre 8148  ax-pre-ltirr 8149  ax-pre-ltwlin 8150  ax-pre-lttrn 8151  ax-pre-ltadd 8153

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-f1 5333  df-fo 5334  df-f1o 5335  df-fv 5336  df-riota 5976  df-ov 6026  df-oprab 6027  df-mpo 6028  df-pnf 8221  df-mnf 8222  df-xr 8223  df-ltxr 8224  df-le 8225  df-sub 8357  df-neg 8358  df-inn 9149  df-n0 9408  df-z 9485  df-uz 9761  df-fz 10249  df-struct 13107  df-slot 13109  df-sets 13112

This theorem is referenced by:  strressid  13177