Metamath Proof Explorer

Theorem setsidvaldOLD

Description: Obsolete version of setsidvald as of 17-Oct-2024. (Contributed by AV, 14-Mar-2020) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	setsidvaldOLD.e	$⊢ E = Slot N$
		setsidvaldOLD.n	$⊢ N \in ℕ$
		setsidvaldOLD.s	$⊢ φ \to S \in V$
		setsidvaldOLD.f	$⊢ φ \to Fun S$
		setsidvaldOLD.d	$⊢ φ \to E (ndx) \in dom S$
	Assertion	setsidvaldOLD	$⊢ φ \to S = S sSet ⟨E (ndx), E (S)⟩$

Proof

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