Theorem setsidvald

Description: Value of the structure replacement function, deduction version.

Hint: Do not substitute N by a specific (positive) integer to be independent of a hard-coded index value. Often, ( Endx ) can be used instead of N . (Contributed by AV, 14-Mar-2020) (Revised by AV, 17-Oct-2024)

	Ref	Expression
Hypotheses	setsidvald.e	$$⊢E=\mathrm{Slot}N$$
	setsidvald.s	$$⊢\phi \to S\in V$$
	setsidvald.f	$$⊢\phi \to \mathrm{Fun}S$$
	setsidvald.d	$$⊢\phi \to N\in \mathrm{dom}S$$
Assertion	setsidvald	$$⊢\phi \to S=S\mathrm{sSet}⟨N,E\left(S\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		setsidvald.e	$$⊢E=\mathrm{Slot}N$$
2		setsidvald.s	$$⊢\phi \to S\in V$$
3		setsidvald.f	$$⊢\phi \to \mathrm{Fun}S$$
4		setsidvald.d	$$⊢\phi \to N\in \mathrm{dom}S$$
5		fvex	$$⊢E\left(S\right)\in \mathrm{V}$$
6		setsval	$$⊢\left(S\in V\wedge E\left(S\right)\in \mathrm{V}\right)\to S\mathrm{sSet}⟨N,E\left(S\right)⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,E\left(S\right)⟩\right\}$$
7	2 5 6	sylancl	$$⊢\phi \to S\mathrm{sSet}⟨N,E\left(S\right)⟩=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,E\left(S\right)⟩\right\}$$
8	1 2	strfvnd	$$⊢\phi \to E\left(S\right)=S\left(N\right)$$
9	8	opeq2d	$$⊢\phi \to ⟨N,E\left(S\right)⟩=⟨N,S\left(N\right)⟩$$
10	9	sneqd	$$⊢\phi \to \left\{⟨N,E\left(S\right)⟩\right\}=\left\{⟨N,S\left(N\right)⟩\right\}$$
11	10	uneq2d	$$⊢\phi \to \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,E\left(S\right)⟩\right\}=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,S\left(N\right)⟩\right\}$$
12		funresdfunsn	$$⊢\left(\mathrm{Fun}S\wedge N\in \mathrm{dom}S\right)\to \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,S\left(N\right)⟩\right\}=S$$
13	3 4 12	syl2anc	$$⊢\phi \to \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \left\{N\right\}\right)}\right)\cup \left\{⟨N,S\left(N\right)⟩\right\}=S$$
14	7 11 13	3eqtrrd	$$⊢\phi \to S=S\mathrm{sSet}⟨N,E\left(S\right)⟩$$