setsnidOLD

Description: Obsolete proof of setsnid as of 7-Nov-2024. Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	setsid.e	$⊢ E = Slot E (ndx)$
	setsnid.n	$⊢ E (ndx) \neq D$
Assertion	setsnidOLD	$⊢ 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		fvprc	$⊢ \neg W \in V \to E (W) = \emptyset$
21		reldmsets	$⊢ Rel dom sSet$
22	21	ovprc1	$⊢ \neg W \in V \to W sSet ⟨D, C⟩ = \emptyset$
23	22	fveq2d	$⊢ \neg W \in V \to E (W sSet ⟨D, C⟩) = E (\emptyset)$
24	19 20 23	3eqtr4a	$⊢ \neg W \in V \to E (W) = E (W sSet ⟨D, C⟩)$
25	18 24	pm2.61i	$⊢ E (W) = E (W sSet ⟨D, C⟩)$

Metamath Proof Explorer

Theorem setsnidOLD

Proof