setsnid

Description: Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 7-Nov-2024)

	Ref	Expression
Hypotheses	setsid.e	$⊢ E = Slot E (ndx)$
	setsnid.n	$⊢ E (ndx) \neq D$
Assertion	setsnid	$⊢ E (W) = E (W sSet ⟨D, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		setsid.e	$⊢ E = Slot E (ndx)$
2		setsnid.n	$⊢ E (ndx) \neq D$
3		id	$⊢ W \in V \to W \in V$
4	1 3	strfvnd	$⊢ W \in V \to E (W) = W (E (ndx))$
5		ovex	$⊢ W sSet ⟨D, C⟩ \in V$
6	5 1	strfvn	$⊢ E (W sSet ⟨D, C⟩) = (W sSet ⟨D, C⟩) (E (ndx))$
7		setsres	$⊢ W \in V \to {(W sSet ⟨D, C⟩) ↾}_{(V ∖ \{D\})} = {W ↾}_{(V ∖ \{D\})}$
8	7	fveq1d	$⊢ W \in V \to ({(W sSet ⟨D, C⟩) ↾}_{(V ∖ \{D\})}) (E (ndx)) = ({W ↾}_{(V ∖ \{D\})}) (E (ndx))$
9		fvex	$⊢ E (ndx) \in V$
10		eldifsn	$⊢ E (ndx) \in (V ∖ \{D\}) \leftrightarrow (E (ndx) \in V \land E (ndx) \neq D)$
11	9 2 10	mpbir2an	$⊢ E (ndx) \in (V ∖ \{D\})$
12		fvres	$⊢ E (ndx) \in (V ∖ \{D\}) \to ({(W sSet ⟨D, C⟩) ↾}_{(V ∖ \{D\})}) (E (ndx)) = (W sSet ⟨D, C⟩) (E (ndx))$
13	11 12	ax-mp	$⊢ ({(W sSet ⟨D, C⟩) ↾}_{(V ∖ \{D\})}) (E (ndx)) = (W sSet ⟨D, C⟩) (E (ndx))$
14		fvres	$⊢ E (ndx) \in (V ∖ \{D\}) \to ({W ↾}_{(V ∖ \{D\})}) (E (ndx)) = W (E (ndx))$
15	11 14	ax-mp	$⊢ ({W ↾}_{(V ∖ \{D\})}) (E (ndx)) = W (E (ndx))$
16	8 13 15	3eqtr3g	$⊢ W \in V \to (W sSet ⟨D, C⟩) (E (ndx)) = W (E (ndx))$
17	6 16	eqtrid	$⊢ W \in V \to E (W sSet ⟨D, C⟩) = W (E (ndx))$
18	4 17	eqtr4d	$⊢ W \in V \to E (W) = E (W sSet ⟨D, C⟩)$
19	1	str0	$⊢ \emptyset = E (\emptyset)$
20	19	eqcomi	$⊢ E (\emptyset) = \emptyset$
21		eqid	$⊢ W sSet ⟨D, C⟩ = W sSet ⟨D, C⟩$
22		reldmsets	$⊢ Rel dom sSet$
23	20 21 22	oveqprc	$⊢ \neg W \in V \to E (W) = E (W sSet ⟨D, C⟩)$
24	18 23	pm2.61i	$⊢ E (W) = E (W sSet ⟨D, C⟩)$

Metamath Proof Explorer

Theorem setsnid

Proof