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 = Slot N$
	setsidvald.s	$⊢ φ \to S \in V$
	setsidvald.f	$⊢ φ \to Fun S$
	setsidvald.d	$⊢ φ \to N \in dom S$
Assertion	setsidvald	$⊢ φ \to S = S sSet ⟨N, E (S)⟩$

Proof

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

Metamath Proof Explorer

Theorem setsidvald

Proof