setsid

Description: Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Hypothesis	setsid.e	$⊢ E = Slot E (ndx)$
	Assertion	setsid	$⊢ (W \in A \land C \in V) \to C = E (W sSet ⟨E (ndx), C⟩)$

Proof

Step	Hyp	Ref	Expression
1		setsid.e	$⊢ E = Slot E (ndx)$
2		setsval	$⊢ (W \in A \land C \in V) \to W sSet ⟨E (ndx), C⟩ = ({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}$
3	2	fveq2d	$⊢ (W \in A \land C \in V) \to E (W sSet ⟨E (ndx), C⟩) = E (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\})$
4		resexg	$⊢ W \in A \to {W ↾}_{(V ∖ \{E (ndx)\})} \in V$
5	4	adantr	$⊢ (W \in A \land C \in V) \to {W ↾}_{(V ∖ \{E (ndx)\})} \in V$
6		snex	$⊢ \{⟨E (ndx), C⟩\} \in V$
7		unexg	$⊢ ({W ↾}_{(V ∖ \{E (ndx)\})} \in V \land \{⟨E (ndx), C⟩\} \in V) \to ({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\} \in V$
8	5 6 7	sylancl	$⊢ (W \in A \land C \in V) \to ({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\} \in V$
9	1 8	strfvnd	$⊢ (W \in A \land C \in V) \to E (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) = (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) (E (ndx))$
10		fvex	$⊢ E (ndx) \in V$
11	10	snid	$⊢ E (ndx) \in \{E (ndx)\}$
12		fvres	$⊢ E (ndx) \in \{E (ndx)\} \to ({(({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) ↾}_{\{E (ndx)\}}) (E (ndx)) = (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) (E (ndx))$
13	11 12	ax-mp	$⊢ ({(({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) ↾}_{\{E (ndx)\}}) (E (ndx)) = (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) (E (ndx))$
14		resres	$⊢ {({W ↾}_{(V ∖ \{E (ndx)\})}) ↾}_{\{E (ndx)\}} = {W ↾}_{((V ∖ \{E (ndx)\}) \cap \{E (ndx)\})}$
15		disjdifr	$⊢ (V ∖ \{E (ndx)\}) \cap \{E (ndx)\} = \emptyset$
16	15	reseq2i	$⊢ {W ↾}_{((V ∖ \{E (ndx)\}) \cap \{E (ndx)\})} = {W ↾}_{\emptyset}$
17		res0	$⊢ {W ↾}_{\emptyset} = \emptyset$
18	16 17	eqtri	$⊢ {W ↾}_{((V ∖ \{E (ndx)\}) \cap \{E (ndx)\})} = \emptyset$
19	14 18	eqtri	$⊢ {({W ↾}_{(V ∖ \{E (ndx)\})}) ↾}_{\{E (ndx)\}} = \emptyset$
20	19	a1i	$⊢ (W \in A \land C \in V) \to {({W ↾}_{(V ∖ \{E (ndx)\})}) ↾}_{\{E (ndx)\}} = \emptyset$
21		elex	$⊢ C \in V \to C \in V$
22	21	adantl	$⊢ (W \in A \land C \in V) \to C \in V$
23		opelxpi	$⊢ (E (ndx) \in V \land C \in V) \to ⟨E (ndx), C⟩ \in (V \times V)$
24	10 22 23	sylancr	$⊢ (W \in A \land C \in V) \to ⟨E (ndx), C⟩ \in (V \times V)$
25		opex	$⊢ ⟨E (ndx), C⟩ \in V$
26	25	relsn	$⊢ Rel \{⟨E (ndx), C⟩\} \leftrightarrow ⟨E (ndx), C⟩ \in (V \times V)$
27	24 26	sylibr	$⊢ (W \in A \land C \in V) \to Rel \{⟨E (ndx), C⟩\}$
28		dmsnopss	$⊢ dom \{⟨E (ndx), C⟩\} \subseteq \{E (ndx)\}$
29		relssres	$⊢ (Rel \{⟨E (ndx), C⟩\} \land dom \{⟨E (ndx), C⟩\} \subseteq \{E (ndx)\}) \to {\{⟨E (ndx), C⟩\} ↾}_{\{E (ndx)\}} = \{⟨E (ndx), C⟩\}$
30	27 28 29	sylancl	$⊢ (W \in A \land C \in V) \to {\{⟨E (ndx), C⟩\} ↾}_{\{E (ndx)\}} = \{⟨E (ndx), C⟩\}$
31	20 30	uneq12d	$⊢ (W \in A \land C \in V) \to ({({W ↾}_{(V ∖ \{E (ndx)\})}) ↾}_{\{E (ndx)\}}) \cup ({\{⟨E (ndx), C⟩\} ↾}_{\{E (ndx)\}}) = \emptyset \cup \{⟨E (ndx), C⟩\}$
32		resundir	$⊢ {(({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) ↾}_{\{E (ndx)\}} = ({({W ↾}_{(V ∖ \{E (ndx)\})}) ↾}_{\{E (ndx)\}}) \cup ({\{⟨E (ndx), C⟩\} ↾}_{\{E (ndx)\}})$
33		un0	$⊢ \{⟨E (ndx), C⟩\} \cup \emptyset = \{⟨E (ndx), C⟩\}$
34		uncom	$⊢ \{⟨E (ndx), C⟩\} \cup \emptyset = \emptyset \cup \{⟨E (ndx), C⟩\}$
35	33 34	eqtr3i	$⊢ \{⟨E (ndx), C⟩\} = \emptyset \cup \{⟨E (ndx), C⟩\}$
36	31 32 35	3eqtr4g	$⊢ (W \in A \land C \in V) \to {(({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) ↾}_{\{E (ndx)\}} = \{⟨E (ndx), C⟩\}$
37	36	fveq1d	$⊢ (W \in A \land C \in V) \to ({(({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) ↾}_{\{E (ndx)\}}) (E (ndx)) = \{⟨E (ndx), C⟩\} (E (ndx))$
38	13 37	eqtr3id	$⊢ (W \in A \land C \in V) \to (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) (E (ndx)) = \{⟨E (ndx), C⟩\} (E (ndx))$
39	10	a1i	$⊢ (W \in A \land C \in V) \to E (ndx) \in V$
40		fvsng	$⊢ (E (ndx) \in V \land C \in V) \to \{⟨E (ndx), C⟩\} (E (ndx)) = C$
41	39 40	sylancom	$⊢ (W \in A \land C \in V) \to \{⟨E (ndx), C⟩\} (E (ndx)) = C$
42	38 41	eqtrd	$⊢ (W \in A \land C \in V) \to (({W ↾}_{(V ∖ \{E (ndx)\})}) \cup \{⟨E (ndx), C⟩\}) (E (ndx)) = C$
43	3 9 42	3eqtrrd	$⊢ (W \in A \land C \in V) \to C = E (W sSet ⟨E (ndx), C⟩)$

Metamath Proof Explorer

Theorem setsid

Proof